Theorem ad2antlr 405

Description: Deduction adding conjuncts to antecedent.

Hypothesis

Ref	Expression
ad2ant.1	|- (ph -> ps)

Assertion

Ref	Expression
ad2antlr	|- (((ch /\ ph) /\ th) -> ps)

Proof of Theorem ad2antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- (ph -> ps)
2	1	adantl 388	. 2 |- ((ch /\ ph) -> ps)
3	2	adantr 389	1 |- (((ch /\ ph) /\ th) -> ps)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  simplr 413  ax11eq 1363  ax11el 1364  tfindsg 3162  caoprord3 4058  oesuc 4166  oelim 4169  oaordi 4180  oaass 4195  odi 4210  omass 4211  oen0 4213  oelim2 4222  undom 4438  xpdom2 4442  mapenlem1 4489  mapenlem2 4490  php3 4515  php3OLD 4516  fiint 4559  fiintOLD 4560  suppr 4590  fodom 4798  unxpdomlem 4843  npex 5091  elnp 5092  cnegext 5348  divdivdivt 5785  lemul12it 5844  lt2mul2divt 5872  lediv12it 5896  lediv2it 5897  xrmax2 5910  xrsupsslem 6076  xrinfmsslem 6077  xrub 6080  supxrre 6083  supxrun 6085  supxrunb1 6089  supxrunb2 6090  supxrbnd 6091  monoord 6294  elioc2t 6390  elico2t 6391  elicc2t 6392  elfzp1 6510  fsequb 6523  sqr11 6703  absmaxt 6897  seq1bnd 6910  cvganz 6924  caubnd 6926  facndivt 6943  faclbnd 6945  sumeq2 6985  fsumcmpndx2 7042  2climnn 7102  2climnn0 7103  climrecl 7110  climsqueeze 7140  climsqueeze2 7141  climsup 7155  climcau 7156  caucvglem6 7162  caucvg 7163  reccnv 7218  cvgratlem2 7251  cvgratlem3 7252  fsum0diaglem2 7257  fsum0diag4 7261  acdc3lem 7486  acdc2lem2 7489  acdc5lem2 7492  acdclem 7494  infxpidmlem12 7563  basgen2t 7639  fctopOLD 7650  elcls3 7711  islp2 7747  iscnp2 7761  cnpco 7769  blss 7853  metcnplem 7886  metcnp 7887  metcni2 7895  metcnp3 7896  metcnss2 7899  tgioolem 7914  lmnn 7935  metcnp4lem2 7969  metcn4 7971  xpcn 7976  bcthlem2 8000  bcthlem13 8011  bcthlem14 8012  bcthlem27 8025  bcthlem28 8026  grpidinv 8052  grpideu 8053  isgrp2i 8076  nvmul0or 8272  sm1cnilem 8347  sspval 8382  nmoub3i 8436  nmo0 8451  blocnilem 8464  blocni 8465  ipblnfi 8516  ubthlem3 8531  ubthlem5 8533  ubthlem13 8541  minveclem27 8571  minveclem31 8575  hvmul0ort 8894  hvaddsub4t 8945  occont 9160  ocorth 9164  occllem6 9178  projlem25 9210  osumlem4 9581  5oalem1 9599  5oalem2 9600  3oalem2 9608  pjds3 9658  nmopub2tALT 9833  nmfnleub2t 9850  hmopadj2t 9865  lnopcon 9963  lnfncon 9990  nlelch 9994  cnlnadjlem6 10005  kbass5t 10053  leopnmidt 10071  nmopleidt 10072  hmopidmch 10079  pjss2co 10092  pjssdif1 10103  pj3cor1 10137  mdsl0 10237  mdslmd1lem1 10252  mdslmd1lem2 10253  csmdsym 10261  superpos 10281  atoml 10309  irredlem2 10318  irredlem3 10319  atcvat3 10323  atcvat4 10324  mdsymlem5 10334  cdjreu 10359  cdj1 10360  cdrci 10494  cnrsfin 10509  cnrscoa 10510  mapdiscn 10511  iintlem1 10632  trnij 10637  cmpasso 10706

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain