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  4626  en2lp  4654  foun  5605  f1oprg  5632  fcof1o  5935  foeqcnvco  5936  f1eqcocnv  5937  caovord3  6201  f1o2ndf1  6398  smores2  6465  frecrdg  6579  nnaordex  6701  xpdom2  7020  xpen  7036  mapen  7037  xpmapenlem  7040  nndomo  7055  phpm  7057  fidifsnen  7062  isinfinf  7091  fidcen  7093  finexdc  7097  elssdc  7099  fientri3  7112  fiintim  7128  xpfi  7129  f1dmvrnfibi  7148  sbthlemi8  7168  djudom  7297  omp1eomlem  7298  difinfsn  7304  ctmlemr  7312  ctssdccl  7315  nnnninfeq  7332  enomnilem  7342  finomni  7344  ismkvnex  7359  enmkvlem  7365  nninfwlpoimlemginf  7380  exmidfodomrlemrALT  7419  exmidontriim  7445  netap  7478  exmidapne  7484  acnccim  7496  dfplpq2  7579  recclnq  7617  subhalfnqq  7639  distrnq0  7684  prarloclem3step  7721  genpml  7742  genpmu  7743  addnqprl  7754  addnqpru  7755  appdivnq  7788  mulnqprl  7793  mulnqpru  7794  mullocpr  7796  ltexprlemfl  7834  ltexprlemfu  7836  ltmprr  7867  archpr  7868  cauappcvgprlemm  7870  caucvgprlemladdrl  7903  caucvgprprlemopl  7922  caucvgprprlemopu  7924  recexgt0sr  7998  mulgt0sr  8003  elrealeu  8054  axcaucvglemcau  8123  axcaucvglemres  8124  cnegex  8362  apirr  8790  mulge0  8804  lemul12a  9047  lediv2a  9080  creur  9144  nndiv  9189  zaddcllemneg  9523  peano5uzti  9593  supinfneg  9834  infsupneg  9835  divfnzn  9860  xrltso  10036  xpncan  10111  xltadd1  10116  xleaddadd  10127  elioc2  10176  elico2  10177  elicc2  10178  exfzdc  10492  zsupcllemstep  10495  infssuzex  10499  suprzubdc  10502  exbtwnzlemex  10515  rebtwn2z  10520  modqid  10617  modqcyc  10627  mulqaddmodid  10632  modqadd2mod  10642  addmodlteq  10666  frecuzrdgg  10684  nninfinf  10711  seq3val  10728  seqvalcd  10729  seq3clss  10739  iseqf1olemqcl  10767  iseqf1olemnab  10769  seq3f1olemp  10783  seq3f1o  10785  seqf1oglem1  10787  seqfeq4g  10799  fser0const  10803  ser3ge0  10804  exp3vallem  10808  qsqeqor  10918  facndiv  11007  faclbnd  11009  bcval5  11031  hashen  11052  fihashdom  11072  hashunlem  11073  hashfacen  11106  zfz1isolemiso  11109  seq3coll  11112  ccatsymb  11188  ccatrn  11195  ccatw2s1p2  11232  swrdccatin1  11315  swrdccatin2  11319  swrdccat3b  11330  caucvgre  11564  resqrexlemlo  11596  cau3lem  11697  qdenre  11785  rexico  11804  fimaxre2  11810  2zinfmin  11826  xrmaxiflemcl  11828  xrmaxifle  11829  xrmaxiflemcom  11832  2clim  11884  cn1lem  11897  climsqz  11918  climsqz2  11919  climcau  11930  sumrbdclem  11961  summodclem2a  11965  fsum3  11971  fsumcl2lem  11982  fsumadd  11990  sumsnf  11993  fsum2dlemstep  12018  fisum0diag2  12031  fsummulc2  12032  mertenslemub  12118  mertenslemi1  12119  mertensabs  12121  ntrivcvgap  12132  prodrbdclem  12155  prodmodclem3  12159  prodmodclem2a  12160  prodmodc  12162  prod1dc  12170  prodsnf  12176  fprod2dlemstep  12206  efaddlem  12258  tanaddaplem  12322  zdvdsdc  12396  dvdseq  12432  dvdsext  12439  odd2np1  12457  sqoddm1div8z  12470  nno  12490  dfgcd3  12604  nninfctlemfo  12634  dvdslcm  12664  lcmneg  12669  lcmgcdlem  12672  ncoprmgcdne1b  12684  qredeq  12691  qredeu  12692  divgcdcoprm0  12696  exprmfct  12733  prmdvdsfz  12734  isprm5  12737  rpexp1i  12749  sqrt2irr  12757  nonsq  12802  eulerthlemrprm  12824  eulerthlema  12825  phisum  12836  modprmn0modprm0  12852  pclemdc  12884  pcz  12928  pcmpt  12939  fldivp1  12944  pcfac  12946  expnprm  12949  oddprmdvds  12950  prmpwdvds  12951  infpnlem1  12955  1arith  12963  4sqlem2  12985  4sqlemafi  12991  4sqleminfi  12993  4sqexercise2  12995  4sqlemsdc  12996  ctinfom  13072  enctlem  13076  nninfdclemlt  13095  setsfun  13140  setsfun0  13141  setscom  13145  gsumfzval  13497  mndissubm  13581  resmhm  13593  resmhm2  13594  mhmco  13596  gsumfzz  13601  gsumwsubmcl  13602  gsumwmhm  13604  dfgrp2  13633  isgrpinv  13660  mulgval  13732  mulgnnp1  13740  mulgz  13760  grpissubg  13804  resghm  13870  qusecsub  13941  isrng  13971  lmodfopne  14364  dflidl2rng  14519  gsumfzfsumlemm  14625  mulgrhm2  14648  znidomb  14696  znunit  14697  psrbaglesuppg  14710  psrbagfi  14712  tgdom  14825  ssrest  14935  cnfval  14947  cnpfval  14948  cnpval  14951  iscnp3  14956  ssidcn  14963  cnpnei  14972  cnntr  14978  cncnp  14983  cnptopresti  14991  tx1cn  15022  upxp  15025  imasnopn  15052  bdmet  15255  metcnp  15265  ivthinclemlr  15390  ivthinclemur  15392  ivthinc  15396  dvrecap  15466  dvmptfsum  15478  elply2  15488  plymullem1  15501  plycolemc  15511  plycjlemc  15513  dvply1  15518  pilem3  15536  relogeftb  15618  logbgcd1irr  15720  mpodvdsmulf1o  15743  mersenne  15750  lgslem4  15761  lgsval  15762  lgsfvalg  15763  lgsval2lem  15768  lgsmod  15784  lgsdir2lem4  15789  lgsdinn0  15806  lgsquad2lem2  15840  lgsquad3  15842  2lgslem1c  15848  2sqlem6  15878  2sqlem7  15879  isupgren  15975  wrdupgren  15976  isumgren  15985  wrdumgren  15986  isuspgren  16037  isusgren  16038  clwwlkext2edg  16302  clwwlknonex2  16319  depindlem3  16388  2omap  16654  pw1map  16656  nnsf  16670  peano4nninf  16671  nninfalllem1  16673  nninfsellemqall  16680  nninfsellemeqinf  16681  nninffeq  16685  exmidsbthrlem  16689  isomninnlem  16701  iswomninnlem  16721  iswomni0  16723  ismkvnnlem  16724