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  6570  frecrdg  6684  nnaordex  6806  xpdom2  7135  xpen  7151  mapen  7152  xpmapenlem  7155  nndomo  7171  phpm  7173  fidifsnen  7178  isinfinf  7207  fidcen  7209  finexdc  7213  elssdc  7215  fientri3  7228  fiintim  7244  xpfi  7245  f1dmvrnfibi  7264  sbthlemi8  7288  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  9692  peano5uzti  9764  supinfneg  10010  infsupneg  10011  divfnzn  10036  xrltso  10214  xpncan  10289  xltadd1  10294  xleaddadd  10305  elioc2  10354  elico2  10355  elicc2  10356  exfzdc  10675  zsupcllemstep  10678  infssuzex  10682  suprzubdc  10687  exbtwnzlemex  10700  rebtwn2z  10705  modqid  10806  modqcyc  10816  mulqaddmodid  10821  modqadd2mod  10831  addmodlteq  10855  frecuzrdgg  10873  nninfinf  10900  seq3val  10917  seqvalcd  10918  seq3clss  10928  iseqf1olemqcl  10956  iseqf1olemnab  10958  seq3f1olemp  10972  seq3f1o  10974  seqf1oglem1  10976  seqfeq4g  10988  fser0const  10992  ser3ge0  10993  exp3vallem  10997  qsqeqor  11107  nn0sqdc  11167  facndiv  11198  faclbnd  11200  bcval5  11222  hashen  11244  fihashdom  11264  hashunlem  11265  hashfacen  11305  zfz1isolemiso  11312  seq3coll  11315  ccatsymb  11391  ccatrn  11398  ccatw2s1p2  11435  swrdccatin1  11518  swrdccatin2  11522  swrdccat3b  11533  caucvgre  11768  resqrexlemlo  11800  cau3lem  11902  qdenre  11990  rexico  12009  fimaxre2  12015  2zinfmin  12033  xrmaxiflemcl  12035  xrmaxifle  12036  xrmaxiflemcom  12039  2clim  12091  cn1lem  12104  climsqz  12125  climsqz2  12126  climcau  12137  sumrbdclem  12168  summodclem2a  12172  fsum3  12178  fsumcl2lem  12189  fsumadd  12197  sumsnf  12200  fsum2dlemstep  12225  fisum0diag2  12238  fsummulc2  12239  mertenslemub  12325  mertenslemi1  12326  mertensabs  12328  ntrivcvgap  12339  prodrbdclem  12362  prodmodclem3  12366  prodmodclem2a  12367  prodmodc  12369  prod1dc  12377  prodsnf  12383  fprod2dlemstep  12413  efaddlem  12465  tanaddaplem  12529  zdvdsdc  12603  dvdseq  12639  dvdsext  12646  odd2np1  12664  sqoddm1div8z  12677  nno  12697  dfgcd3  12811  nninfctlemfo  12841  dvdslcm  12871  lcmneg  12876  lcmgcdlem  12879  ncoprmgcdne1b  12891  qredeq  12898  qredeu  12899  divgcdcoprm0  12903  exprmfct  12941  prmdvdsfz  12942  isprm5  12945  rpexp1i  12957  sqrt2irr  12965  nonsq  13011  sqrtrirr  13013  eulerthlemrprm  13035  eulerthlema  13036  phisum  13047  modprmn0modprm0  13063  pclemdc  13095  pcz  13139  pcmpt  13150  fldivp1  13155  pcfac  13157  expnprm  13160  oddprmdvds  13161  prmpwdvds  13162  infpnlem1  13166  1arith  13174  4sqlem2  13196  4sqlemafi  13202  4sqleminfi  13204  4sqexercise2  13206  4sqlemsdc  13207  ballotfilemsv  13310  ballotfilemsima  13316  ctinfom  13376  enctlem  13380  nninfdclemlt  13399  setsfun  13444  setsfun0  13445  setscom  13449  gzsumfzval  13769  mndissubm  13840  resmhm  13852  resmhm2  13853  mhmco  13855  gzsumwsubmcl  13859  gzsumwmhm  13861  dfgrp2  13890  isgrpinv  13917  mulgval  13983  mulgnnp1  13991  mulgz  14011  grpissubg  14055  resghm  14121  cntzsgrpcl  14166  cntzsubm  14169  cntzmhm  14172  qusecsub  14224  gsumf1ofi  14249  isrng  14339  lmodfopne  14771  dflidl2rng  14926  mulgrhm2  15053  znidomb  15101  znunit  15102  issubassa2  15143  psrbagfi  15166  psrbaglesuppg  15170  tgdom  15315  ssrest  15425  cnfval  15437  cnpfval  15438  cnpval  15441  iscnp3  15446  ssidcn  15453  cnpnei  15462  cnntr  15468  cncnp  15473  cnptopresti  15481  tx1cn  15512  upxp  15515  imasnopn  15542  bdmet  15745  metcnp  15755  ivthinclemlr  15880  ivthinclemur  15882  ivthinc  15886  dvrecap  15956  dvmptfsum  15968  elply2  15978  plymullem1  15991  plycolemc  16001  plycjlemc  16003  dvply1  16008  pilem3  16027  relogeftb  16111  logbgcd1irr  16220  birthdaylem3  16244  mpodvdsmulf1o  16301  chtublem  16312  mersenne  16314  bposlem1  16328  bposlem3  16330  bposlem5  16332  lgslem4  16344  lgsval  16345  lgsfvalg  16346  lgsval2lem  16351  lgsmod  16367  lgsdir2lem4  16372  lgsdinn0  16389  lgsquad2lem2  16423  lgsquad3  16425  2lgslem1c  16431  2sqlem6  16461  2sqlem7  16462  isupgren  16558  wrdupgren  16559  isumgren  16568  wrdumgren  16569  isuspgren  16620  isusgren  16621  clwwlkext2edg  16885  clwwlknonex2  16902  depindlem3  16971  pw1map  17247  nnsf  17271  peano4nninf  17272  nninfalllem1  17274  nninfsellemqall  17281  nninfsellemeqinf  17282  nninffeq  17286  exmidsbthrlem  17290  isomninnlem  17302  iswomninnlem  17323  iswomni0  17325  ismkvnnlem  17326