Theorem ad2antlr 493

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  ad3antlr  497  simplr  533  simplrl  541  simplrr  542  ordtri2or2exmidlem  4668  en2lp  4696  foun  5653  f1oprg  5680  fcof1o  5985  foeqcnvco  5986  f1eqcocnv  5987  caovord3  6253  f1o2ndf1  6454  suppfnss  6487  suppssdc  6490  suppssfvg  6493  smores2  6555  frecrdg  6669  nnaordex  6791  xpdom2  7119  xpen  7135  mapen  7136  xpmapenlem  7139  nndomo  7155  phpm  7157  fidifsnen  7162  isinfinf  7191  fidcen  7193  finexdc  7197  elssdc  7199  fientri3  7212  fiintim  7228  xpfi  7229  f1dmvrnfibi  7248  sbthlemi8  7271  2omap  7308  2omapfi  7310  djudom  7423  omp1eomlem  7424  difinfsn  7430  ctmlemr  7438  ctssdccl  7441  nnnninfeq  7458  enomnilem  7468  finomni  7470  ismkvnex  7485  enmkvlem  7491  nninfwlpoimlemginf  7506  exmidfodomrlemrALT  7545  exmidontriim  7571  netap  7610  exmidapne  7616  acnccim  7628  dfplpq2  7711  recclnq  7749  subhalfnqq  7771  distrnq0  7816  prarloclem3step  7853  genpml  7874  genpmu  7875  addnqprl  7886  addnqpru  7887  appdivnq  7920  mulnqprl  7925  mulnqpru  7926  mullocpr  7928  ltexprlemfl  7966  ltexprlemfu  7968  ltmprr  7999  archpr  8000  cauappcvgprlemm  8002  caucvgprlemladdrl  8035  caucvgprprlemopl  8054  caucvgprprlemopu  8056  recexgt0sr  8130  mulgt0sr  8135  elrealeu  8186  axcaucvglemcau  8255  axcaucvglemres  8256  cnegex  8494  apirr  8923  mulge0  8937  lemul12a  9182  lediv2a  9215  creur  9279  nndiv  9324  zaddcllemneg  9662  peano5uzti  9733  supinfneg  9974  infsupneg  9975  divfnzn  10000  xrltso  10177  xpncan  10252  xltadd1  10257  xleaddadd  10268  elioc2  10317  elico2  10318  elicc2  10319  exfzdc  10637  zsupcllemstep  10640  infssuzex  10644  suprzubdc  10649  exbtwnzlemex  10662  rebtwn2z  10667  modqid  10764  modqcyc  10774  mulqaddmodid  10779  modqadd2mod  10789  addmodlteq  10813  frecuzrdgg  10831  nninfinf  10858  seq3val  10875  seqvalcd  10876  seq3clss  10886  iseqf1olemqcl  10914  iseqf1olemnab  10916  seq3f1olemp  10930  seq3f1o  10932  seqf1oglem1  10934  seqfeq4g  10946  fser0const  10950  ser3ge0  10951  exp3vallem  10955  qsqeqor  11065  facndiv  11155  faclbnd  11157  bcval5  11179  hashen  11201  fihashdom  11221  hashunlem  11222  hashfacen  11262  zfz1isolemiso  11269  seq3coll  11272  ccatsymb  11348  ccatrn  11355  ccatw2s1p2  11392  swrdccatin1  11475  swrdccatin2  11479  swrdccat3b  11490  caucvgre  11725  resqrexlemlo  11757  cau3lem  11858  qdenre  11946  rexico  11965  fimaxre2  11971  2zinfmin  11987  xrmaxiflemcl  11989  xrmaxifle  11990  xrmaxiflemcom  11993  2clim  12045  cn1lem  12058  climsqz  12079  climsqz2  12080  climcau  12091  sumrbdclem  12122  summodclem2a  12126  fsum3  12132  fsumcl2lem  12143  fsumadd  12151  sumsnf  12154  fsum2dlemstep  12179  fisum0diag2  12192  fsummulc2  12193  mertenslemub  12279  mertenslemi1  12280  mertensabs  12282  ntrivcvgap  12293  prodrbdclem  12316  prodmodclem3  12320  prodmodclem2a  12321  prodmodc  12323  prod1dc  12331  prodsnf  12337  fprod2dlemstep  12367  efaddlem  12419  tanaddaplem  12483  zdvdsdc  12557  dvdseq  12593  dvdsext  12600  odd2np1  12618  sqoddm1div8z  12631  nno  12651  dfgcd3  12765  nninfctlemfo  12795  dvdslcm  12825  lcmneg  12830  lcmgcdlem  12833  ncoprmgcdne1b  12845  qredeq  12852  qredeu  12853  divgcdcoprm0  12857  exprmfct  12894  prmdvdsfz  12895  isprm5  12898  rpexp1i  12910  sqrt2irr  12918  nonsq  12963  eulerthlemrprm  12985  eulerthlema  12986  phisum  12997  modprmn0modprm0  13013  pclemdc  13045  pcz  13089  pcmpt  13100  fldivp1  13105  pcfac  13107  expnprm  13110  oddprmdvds  13111  prmpwdvds  13112  infpnlem1  13116  1arith  13124  4sqlem2  13146  4sqlemafi  13152  4sqleminfi  13154  4sqexercise2  13156  4sqlemsdc  13157  ballotfilemsv  13231  ballotfilemsima  13237  ctinfom  13297  enctlem  13301  nninfdclemlt  13320  setsfun  13365  setsfun0  13366  setscom  13370  gzsumfzval  13688  mndissubm  13759  resmhm  13771  resmhm2  13772  mhmco  13774  gzsumwsubmcl  13778  gzsumwmhm  13780  dfgrp2  13809  isgrpinv  13836  mulgval  13902  mulgnnp1  13910  mulgz  13930  grpissubg  13974  resghm  14040  qusecsub  14112  gsumf1ofi  14137  isrng  14208  lmodfopne  14635  dflidl2rng  14790  mulgrhm2  14917  znidomb  14965  znunit  14966  psrbaglesuppg  14980  psrbagfi  14982  tgdom  15096  ssrest  15206  cnfval  15218  cnpfval  15219  cnpval  15222  iscnp3  15227  ssidcn  15234  cnpnei  15243  cnntr  15249  cncnp  15254  cnptopresti  15262  tx1cn  15293  upxp  15296  imasnopn  15323  bdmet  15526  metcnp  15536  ivthinclemlr  15661  ivthinclemur  15663  ivthinc  15667  dvrecap  15737  dvmptfsum  15749  elply2  15759  plymullem1  15772  plycolemc  15782  plycjlemc  15784  dvply1  15789  pilem3  15807  relogeftb  15889  logbgcd1irr  15992  mpodvdsmulf1o  16018  mersenne  16025  lgslem4  16036  lgsval  16037  lgsfvalg  16038  lgsval2lem  16043  lgsmod  16059  lgsdir2lem4  16064  lgsdinn0  16081  lgsquad2lem2  16115  lgsquad3  16117  2lgslem1c  16123  2sqlem6  16153  2sqlem7  16154  isupgren  16250  wrdupgren  16251  isumgren  16260  wrdumgren  16261  isuspgren  16312  isusgren  16313  clwwlkext2edg  16577  clwwlknonex2  16594  depindlem3  16663  pw1map  16939  nnsf  16953  peano4nninf  16954  nninfalllem1  16956  nninfsellemqall  16963  nninfsellemeqinf  16964  nninffeq  16968  exmidsbthrlem  16972  isomninnlem  16984  iswomninnlem  17004  iswomni0  17006  ismkvnnlem  17007