Theorem ad2antlr 486

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)

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	adantr 274	. 2 |- ( ( ph /\ th ) -> ps )
3	2	adantll 473	1 |- ( ( ( ch /\ ph ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad3antlr  490  simplr  525  simplrl  530  simplrr  531  ordtri2or2exmidlem  4510  en2lp  4538  foun  5461  f1oprg  5486  fcof1o  5768  foeqcnvco  5769  f1eqcocnv  5770  caovord3  6026  f1o2ndf1  6207  smores2  6273  frecrdg  6387  nnaordex  6507  xpdom2  6809  xpen  6823  mapen  6824  xpmapenlem  6827  nndomo  6842  phpm  6843  fidifsnen  6848  isinfinf  6875  finexdc  6880  fientri3  6892  fiintim  6906  xpfi  6907  f1dmvrnfibi  6921  sbthlemi8  6941  djudom  7070  omp1eomlem  7071  difinfsn  7077  ctmlemr  7085  ctssdccl  7088  nnnninfeq  7104  enomnilem  7114  finomni  7116  ismkvnex  7131  enmkvlem  7137  nninfwlpoimlemginf  7152  exmidfodomrlemrALT  7180  exmidontriim  7202  dfplpq2  7316  recclnq  7354  subhalfnqq  7376  distrnq0  7421  prarloclem3step  7458  genpml  7479  genpmu  7480  addnqprl  7491  addnqpru  7492  appdivnq  7525  mulnqprl  7530  mulnqpru  7531  mullocpr  7533  ltexprlemfl  7571  ltexprlemfu  7573  ltmprr  7604  archpr  7605  cauappcvgprlemm  7607  caucvgprlemladdrl  7640  caucvgprprlemopl  7659  caucvgprprlemopu  7661  recexgt0sr  7735  mulgt0sr  7740  elrealeu  7791  axcaucvglemcau  7860  axcaucvglemres  7861  cnegex  8097  apirr  8524  mulge0  8538  lemul12a  8778  lediv2a  8811  creur  8875  nndiv  8919  zaddcllemneg  9251  peano5uzti  9320  supinfneg  9554  infsupneg  9555  divfnzn  9580  xrltso  9753  xpncan  9828  xltadd1  9833  xleaddadd  9844  elioc2  9893  elico2  9894  elicc2  9895  exfzdc  10196  exbtwnzlemex  10206  rebtwn2z  10211  modqid  10305  modqcyc  10315  mulqaddmodid  10320  modqadd2mod  10330  addmodlteq  10354  frecuzrdgg  10372  seq3val  10414  seqvalcd  10415  seq3clss  10423  iseqf1olemqcl  10442  iseqf1olemnab  10444  seq3f1olemp  10458  seq3f1o  10460  fser0const  10472  ser3ge0  10473  exp3vallem  10477  qsqeqor  10586  facndiv  10673  faclbnd  10675  bcval5  10697  hashen  10718  fihashdom  10738  hashunlem  10739  hashfacen  10771  zfz1isolemiso  10774  seq3coll  10777  caucvgre  10945  resqrexlemlo  10977  cau3lem  11078  qdenre  11166  rexico  11185  fimaxre2  11190  2zinfmin  11206  xrmaxiflemcl  11208  xrmaxifle  11209  xrmaxiflemcom  11212  2clim  11264  cn1lem  11277  climsqz  11298  climsqz2  11299  climcau  11310  sumrbdclem  11340  summodclem2a  11344  fsum3  11350  fsumcl2lem  11361  fsumadd  11369  sumsnf  11372  fsum2dlemstep  11397  fisum0diag2  11410  fsummulc2  11411  mertenslemub  11497  mertenslemi1  11498  mertensabs  11500  ntrivcvgap  11511  prodrbdclem  11534  prodmodclem3  11538  prodmodclem2a  11539  prodmodc  11541  prod1dc  11549  prodsnf  11555  fprod2dlemstep  11585  efaddlem  11637  tanaddaplem  11701  zdvdsdc  11774  dvdseq  11808  dvdsext  11815  odd2np1  11832  sqoddm1div8z  11845  nno  11865  zsupcllemstep  11900  infssuzex  11904  suprzubdc  11907  dfgcd3  11965  dvdslcm  12023  lcmneg  12028  lcmgcdlem  12031  ncoprmgcdne1b  12043  qredeq  12050  qredeu  12051  divgcdcoprm0  12055  exprmfct  12092  prmdvdsfz  12093  isprm5  12096  rpexp1i  12108  sqrt2irr  12116  nonsq  12161  eulerthlemrprm  12183  eulerthlema  12184  phisum  12194  modprmn0modprm0  12210  pclemdc  12242  pcz  12285  pcmpt  12295  fldivp1  12300  pcfac  12302  expnprm  12305  oddprmdvds  12306  prmpwdvds  12307  infpnlem1  12311  1arith  12319  4sqlem2  12341  ctinfom  12383  enctlem  12387  nninfdclemlt  12406  setsfun  12451  setsfun0  12452  setscom  12456  mndissubm  12697  mhmco  12705  dfgrp2  12732  isgrpinv  12756  tgdom  12866  ssrest  12976  cnfval  12988  cnpfval  12989  cnpval  12992  iscnp3  12997  ssidcn  13004  cnpnei  13013  cnntr  13019  cncnp  13024  cnptopresti  13032  tx1cn  13063  upxp  13066  imasnopn  13093  bdmet  13296  metcnp  13306  ivthinclemlr  13409  ivthinclemur  13411  ivthinc  13415  dvrecap  13471  pilem3  13498  relogeftb  13580  logbgcd1irr  13679  lgslem4  13698  lgsval  13699  lgsfvalg  13700  lgsval2lem  13705  lgsmod  13721  lgsdir2lem4  13726  lgsdinn0  13743  2sqlem6  13750  2sqlem7  13751  nnsf  14038  peano4nninf  14039  nninfalllem1  14041  nninfsellemqall  14048  nninfsellemeqinf  14049  nninffeq  14053  exmidsbthrlem  14054  isomninnlem  14062  iswomninnlem  14081  iswomni0  14083  ismkvnnlem  14084