Theorem ad2antlr 489

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	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad2antlr	⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)

Proof of Theorem ad2antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 276	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜓)
3	2	adantll 476	1 ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)

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  493  simplr  529  simplrl  537  simplrr  538  ordtri2or2exmidlem  4650  en2lp  4678  foun  5635  f1oprg  5662  fcof1o  5964  foeqcnvco  5965  f1eqcocnv  5966  caovord3  6230  f1o2ndf1  6426  suppfnss  6459  suppssdc  6462  suppssfvg  6465  smores2  6527  frecrdg  6641  nnaordex  6763  xpdom2  7084  xpen  7100  mapen  7101  xpmapenlem  7104  nndomo  7120  phpm  7122  fidifsnen  7127  isinfinf  7156  fidcen  7158  finexdc  7162  elssdc  7164  fientri3  7177  fiintim  7193  xpfi  7194  f1dmvrnfibi  7213  sbthlemi8  7236  2omap  7271  2omapfi  7273  djudom  7386  omp1eomlem  7387  difinfsn  7393  ctmlemr  7401  ctssdccl  7404  nnnninfeq  7421  enomnilem  7431  finomni  7433  ismkvnex  7448  enmkvlem  7454  nninfwlpoimlemginf  7469  exmidfodomrlemrALT  7508  exmidontriim  7534  netap  7573  exmidapne  7579  acnccim  7591  dfplpq2  7674  recclnq  7712  subhalfnqq  7734  distrnq0  7779  prarloclem3step  7816  genpml  7837  genpmu  7838  addnqprl  7849  addnqpru  7850  appdivnq  7883  mulnqprl  7888  mulnqpru  7889  mullocpr  7891  ltexprlemfl  7929  ltexprlemfu  7931  ltmprr  7962  archpr  7963  cauappcvgprlemm  7965  caucvgprlemladdrl  7998  caucvgprprlemopl  8017  caucvgprprlemopu  8019  recexgt0sr  8093  mulgt0sr  8098  elrealeu  8149  axcaucvglemcau  8218  axcaucvglemres  8219  cnegex  8456  apirr  8884  mulge0  8898  lemul12a  9141  lediv2a  9174  creur  9238  nndiv  9283  zaddcllemneg  9621  peano5uzti  9692  supinfneg  9933  infsupneg  9934  divfnzn  9959  xrltso  10135  xpncan  10210  xltadd1  10215  xleaddadd  10226  elioc2  10275  elico2  10276  elicc2  10277  exfzdc  10593  zsupcllemstep  10596  infssuzex  10600  suprzubdc  10603  exbtwnzlemex  10616  rebtwn2z  10621  modqid  10718  modqcyc  10728  mulqaddmodid  10733  modqadd2mod  10743  addmodlteq  10767  frecuzrdgg  10785  nninfinf  10812  seq3val  10829  seqvalcd  10830  seq3clss  10840  iseqf1olemqcl  10868  iseqf1olemnab  10870  seq3f1olemp  10884  seq3f1o  10886  seqf1oglem1  10888  seqfeq4g  10900  fser0const  10904  ser3ge0  10905  exp3vallem  10909  qsqeqor  11019  facndiv  11109  faclbnd  11111  bcval5  11133  hashen  11155  fihashdom  11175  hashunlem  11176  hashfacen  11216  zfz1isolemiso  11219  seq3coll  11222  ccatsymb  11298  ccatrn  11305  ccatw2s1p2  11342  swrdccatin1  11425  swrdccatin2  11429  swrdccat3b  11440  caucvgre  11674  resqrexlemlo  11706  cau3lem  11807  qdenre  11895  rexico  11914  fimaxre2  11920  2zinfmin  11936  xrmaxiflemcl  11938  xrmaxifle  11939  xrmaxiflemcom  11942  2clim  11994  cn1lem  12007  climsqz  12028  climsqz2  12029  climcau  12040  sumrbdclem  12071  summodclem2a  12075  fsum3  12081  fsumcl2lem  12092  fsumadd  12100  sumsnf  12103  fsum2dlemstep  12128  fisum0diag2  12141  fsummulc2  12142  mertenslemub  12228  mertenslemi1  12229  mertensabs  12231  ntrivcvgap  12242  prodrbdclem  12265  prodmodclem3  12269  prodmodclem2a  12270  prodmodc  12272  prod1dc  12280  prodsnf  12286  fprod2dlemstep  12316  efaddlem  12368  tanaddaplem  12432  zdvdsdc  12506  dvdseq  12542  dvdsext  12549  odd2np1  12567  sqoddm1div8z  12580  nno  12600  dfgcd3  12714  nninfctlemfo  12744  dvdslcm  12774  lcmneg  12779  lcmgcdlem  12782  ncoprmgcdne1b  12794  qredeq  12801  qredeu  12802  divgcdcoprm0  12806  exprmfct  12843  prmdvdsfz  12844  isprm5  12847  rpexp1i  12859  sqrt2irr  12867  nonsq  12912  eulerthlemrprm  12934  eulerthlema  12935  phisum  12946  modprmn0modprm0  12962  pclemdc  12994  pcz  13038  pcmpt  13049  fldivp1  13054  pcfac  13056  expnprm  13059  oddprmdvds  13060  prmpwdvds  13061  infpnlem1  13065  1arith  13073  4sqlem2  13095  4sqlemafi  13101  4sqleminfi  13103  4sqexercise2  13105  4sqlemsdc  13106  ctinfom  13200  enctlem  13204  nninfdclemlt  13223  setsfun  13268  setsfun0  13269  setscom  13273  gsumfzval  13625  mndissubm  13709  resmhm  13721  resmhm2  13722  mhmco  13724  gsumfzz  13729  gsumwsubmcl  13730  gsumwmhm  13732  dfgrp2  13761  isgrpinv  13788  mulgval  13860  mulgnnp1  13868  mulgz  13888  grpissubg  13932  resghm  13998  qusecsub  14069  isrng  14099  lmodfopne  14523  dflidl2rng  14678  gsumfzfsumlemm  14784  mulgrhm2  14807  znidomb  14855  znunit  14856  psrbaglesuppg  14870  psrbagfi  14872  tgdom  14986  ssrest  15096  cnfval  15108  cnpfval  15109  cnpval  15112  iscnp3  15117  ssidcn  15124  cnpnei  15133  cnntr  15139  cncnp  15144  cnptopresti  15152  tx1cn  15183  upxp  15186  imasnopn  15213  bdmet  15416  metcnp  15426  ivthinclemlr  15551  ivthinclemur  15553  ivthinc  15557  dvrecap  15627  dvmptfsum  15639  elply2  15649  plymullem1  15662  plycolemc  15672  plycjlemc  15674  dvply1  15679  pilem3  15697  relogeftb  15779  logbgcd1irr  15881  mpodvdsmulf1o  15907  mersenne  15914  lgslem4  15925  lgsval  15926  lgsfvalg  15927  lgsval2lem  15932  lgsmod  15948  lgsdir2lem4  15953  lgsdinn0  15970  lgsquad2lem2  16004  lgsquad3  16006  2lgslem1c  16012  2sqlem6  16042  2sqlem7  16043  isupgren  16139  wrdupgren  16140  isumgren  16149  wrdumgren  16150  isuspgren  16201  isusgren  16202  clwwlkext2edg  16466  clwwlknonex2  16483  depindlem3  16552  pw1map  16818  nnsf  16832  peano4nninf  16833  nninfalllem1  16835  nninfsellemqall  16842  nninfsellemeqinf  16843  nninffeq  16847  exmidsbthrlem  16851  isomninnlem  16863  iswomninnlem  16883  iswomni0  16885  ismkvnnlem  16886