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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad3antlr  497  simplr  533  simplrl  541  simplrr  542  ordtri2or2exmidlem  4675  en2lp  4703  foun  5661  f1oprg  5688  fcof1o  5998  foeqcnvco  5999  f1eqcocnv  6000  caovord3  6266  f1o2ndf1  6468  suppfnss  6501  suppssdc  6504  suppssfvg  6507  smores2  6569  frecrdg  6683  nnaordex  6805  xpdom2  7133  xpen  7149  mapen  7150  xpmapenlem  7153  nndomo  7169  phpm  7171  fidifsnen  7176  isinfinf  7205  fidcen  7207  finexdc  7211  elssdc  7213  fientri3  7226  fiintim  7242  xpfi  7243  f1dmvrnfibi  7262  sbthlemi8  7286  2omap  7324  2omapfi  7326  djudom  7439  omp1eomlem  7440  difinfsn  7446  ctmlemr  7454  ctssdccl  7457  nnnninfeq  7474  enomnilem  7484  finomni  7486  ismkvnex  7501  enmkvlem  7507  nninfwlpoimlemginf  7522  exmidfodomrlemrALT  7561  exmidontriim  7587  netap  7626  exmidapne  7632  acnccim  7644  dfplpq2  7727  recclnq  7765  subhalfnqq  7787  distrnq0  7832  prarloclem3step  7869  genpml  7890  genpmu  7891  addnqprl  7902  addnqpru  7903  appdivnq  7936  mulnqprl  7941  mulnqpru  7942  mullocpr  7944  ltexprlemfl  7982  ltexprlemfu  7984  ltmprr  8015  archpr  8016  cauappcvgprlemm  8018  caucvgprlemladdrl  8051  caucvgprprlemopl  8070  caucvgprprlemopu  8072  recexgt0sr  8146  mulgt0sr  8151  elrealeu  8202  axcaucvglemcau  8271  axcaucvglemres  8272  cnegex  8511  apirr  8941  mulge0  8955  lemul12a  9200  lediv2a  9233  creur  9297  nndiv  9354  zaddcllemneg  9694  peano5uzti  9765  supinfneg  10011  infsupneg  10012  divfnzn  10037  xrltso  10215  xpncan  10290  xltadd1  10295  xleaddadd  10306  elioc2  10355  elico2  10356  elicc2  10357  exfzdc  10676  zsupcllemstep  10679  infssuzex  10683  suprzubdc  10688  exbtwnzlemex  10701  rebtwn2z  10706  modqid  10807  modqcyc  10817  mulqaddmodid  10822  modqadd2mod  10832  addmodlteq  10856  frecuzrdgg  10874  nninfinf  10901  seq3val  10918  seqvalcd  10919  seq3clss  10929  iseqf1olemqcl  10957  iseqf1olemnab  10959  seq3f1olemp  10973  seq3f1o  10975  seqf1oglem1  10977  seqfeq4g  10989  fser0const  10993  ser3ge0  10994  exp3vallem  10998  qsqeqor  11108  nn0sqdc  11168  facndiv  11199  faclbnd  11201  bcval5  11223  hashen  11245  fihashdom  11265  hashunlem  11266  hashfacen  11306  zfz1isolemiso  11313  seq3coll  11316  ccatsymb  11392  ccatrn  11399  ccatw2s1p2  11436  swrdccatin1  11519  swrdccatin2  11523  swrdccat3b  11534  caucvgre  11769  resqrexlemlo  11801  cau3lem  11903  qdenre  11991  rexico  12010  fimaxre2  12016  2zinfmin  12034  xrmaxiflemcl  12036  xrmaxifle  12037  xrmaxiflemcom  12040  2clim  12092  cn1lem  12105  climsqz  12126  climsqz2  12127  climcau  12138  sumrbdclem  12169  summodclem2a  12173  fsum3  12179  fsumcl2lem  12190  fsumadd  12198  sumsnf  12201  fsum2dlemstep  12226  fisum0diag2  12239  fsummulc2  12240  mertenslemub  12326  mertenslemi1  12327  mertensabs  12329  ntrivcvgap  12340  prodrbdclem  12363  prodmodclem3  12367  prodmodclem2a  12368  prodmodc  12370  prod1dc  12378  prodsnf  12384  fprod2dlemstep  12414  efaddlem  12466  tanaddaplem  12530  zdvdsdc  12604  dvdseq  12640  dvdsext  12647  odd2np1  12665  sqoddm1div8z  12678  nno  12698  dfgcd3  12812  nninfctlemfo  12842  dvdslcm  12872  lcmneg  12877  lcmgcdlem  12880  ncoprmgcdne1b  12892  qredeq  12899  qredeu  12900  divgcdcoprm0  12904  exprmfct  12942  prmdvdsfz  12943  isprm5  12946  rpexp1i  12958  sqrt2irr  12966  nonsq  13012  sqrtrirr  13014  eulerthlemrprm  13036  eulerthlema  13037  phisum  13048  modprmn0modprm0  13064  pclemdc  13096  pcz  13140  pcmpt  13151  fldivp1  13156  pcfac  13158  expnprm  13161  oddprmdvds  13162  prmpwdvds  13163  infpnlem1  13167  1arith  13175  4sqlem2  13197  4sqlemafi  13203  4sqleminfi  13205  4sqexercise2  13207  4sqlemsdc  13208  ballotfilemsv  13311  ballotfilemsima  13317  ctinfom  13377  enctlem  13381  nninfdclemlt  13400  setsfun  13445  setsfun0  13446  setscom  13450  gzsumfzval  13770  mndissubm  13841  resmhm  13853  resmhm2  13854  mhmco  13856  gzsumwsubmcl  13860  gzsumwmhm  13862  dfgrp2  13891  isgrpinv  13918  mulgval  13984  mulgnnp1  13992  mulgz  14012  grpissubg  14056  resghm  14122  cntzsgrpcl  14167  cntzsubm  14170  cntzmhm  14173  qusecsub  14225  gsumf1ofi  14250  isrng  14340  lmodfopne  14772  dflidl2rng  14927  mulgrhm2  15054  znidomb  15102  znunit  15103  issubassa2  15144  psrbaglesuppg  15166  psrbagfi  15168  tgdom  15298  ssrest  15408  cnfval  15420  cnpfval  15421  cnpval  15424  iscnp3  15429  ssidcn  15436  cnpnei  15445  cnntr  15451  cncnp  15456  cnptopresti  15464  tx1cn  15495  upxp  15498  imasnopn  15525  bdmet  15728  metcnp  15738  ivthinclemlr  15863  ivthinclemur  15865  ivthinc  15869  dvrecap  15939  dvmptfsum  15951  elply2  15961  plymullem1  15974  plycolemc  15984  plycjlemc  15986  dvply1  15991  pilem3  16010  relogeftb  16094  logbgcd1irr  16203  birthdaylem3  16227  mpodvdsmulf1o  16284  chtublem  16295  mersenne  16297  bposlem1  16311  bposlem3  16313  bposlem5  16315  lgslem4  16327  lgsval  16328  lgsfvalg  16329  lgsval2lem  16334  lgsmod  16350  lgsdir2lem4  16355  lgsdinn0  16372  lgsquad2lem2  16406  lgsquad3  16408  2lgslem1c  16414  2sqlem6  16444  2sqlem7  16445  isupgren  16541  wrdupgren  16542  isumgren  16551  wrdumgren  16552  isuspgren  16603  isusgren  16604  clwwlkext2edg  16868  clwwlknonex2  16885  depindlem3  16954  pw1map  17230  nnsf  17254  peano4nninf  17255  nninfalllem1  17257  nninfsellemqall  17264  nninfsellemeqinf  17265  nninffeq  17269  exmidsbthrlem  17273  isomninnlem  17285  iswomninnlem  17306  iswomni0  17308  ismkvnnlem  17309