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  528  simplrl  535  simplrr  536  ordtri2or2exmidlem  4622  en2lp  4650  foun  5599  f1oprg  5625  fcof1o  5925  foeqcnvco  5926  f1eqcocnv  5927  caovord3  6191  f1o2ndf1  6388  smores2  6455  frecrdg  6569  nnaordex  6691  xpdom2  7010  xpen  7026  mapen  7027  xpmapenlem  7030  nndomo  7045  phpm  7047  fidifsnen  7052  isinfinf  7081  fidcen  7083  finexdc  7087  elssdc  7089  fientri3  7102  fiintim  7118  xpfi  7119  f1dmvrnfibi  7137  sbthlemi8  7157  djudom  7286  omp1eomlem  7287  difinfsn  7293  ctmlemr  7301  ctssdccl  7304  nnnninfeq  7321  enomnilem  7331  finomni  7333  ismkvnex  7348  enmkvlem  7354  nninfwlpoimlemginf  7369  exmidfodomrlemrALT  7407  exmidontriim  7433  netap  7466  exmidapne  7472  acnccim  7484  dfplpq2  7567  recclnq  7605  subhalfnqq  7627  distrnq0  7672  prarloclem3step  7709  genpml  7730  genpmu  7731  addnqprl  7742  addnqpru  7743  appdivnq  7776  mulnqprl  7781  mulnqpru  7782  mullocpr  7784  ltexprlemfl  7822  ltexprlemfu  7824  ltmprr  7855  archpr  7856  cauappcvgprlemm  7858  caucvgprlemladdrl  7891  caucvgprprlemopl  7910  caucvgprprlemopu  7912  recexgt0sr  7986  mulgt0sr  7991  elrealeu  8042  axcaucvglemcau  8111  axcaucvglemres  8112  cnegex  8350  apirr  8778  mulge0  8792  lemul12a  9035  lediv2a  9068  creur  9132  nndiv  9177  zaddcllemneg  9511  peano5uzti  9581  supinfneg  9822  infsupneg  9823  divfnzn  9848  xrltso  10024  xpncan  10099  xltadd1  10104  xleaddadd  10115  elioc2  10164  elico2  10165  elicc2  10166  exfzdc  10479  zsupcllemstep  10482  infssuzex  10486  suprzubdc  10489  exbtwnzlemex  10502  rebtwn2z  10507  modqid  10604  modqcyc  10614  mulqaddmodid  10619  modqadd2mod  10629  addmodlteq  10653  frecuzrdgg  10671  nninfinf  10698  seq3val  10715  seqvalcd  10716  seq3clss  10726  iseqf1olemqcl  10754  iseqf1olemnab  10756  seq3f1olemp  10770  seq3f1o  10772  seqf1oglem1  10774  seqfeq4g  10786  fser0const  10790  ser3ge0  10791  exp3vallem  10795  qsqeqor  10905  facndiv  10994  faclbnd  10996  bcval5  11018  hashen  11039  fihashdom  11059  hashunlem  11060  hashfacen  11093  zfz1isolemiso  11096  seq3coll  11099  ccatsymb  11172  ccatrn  11179  ccatw2s1p2  11216  swrdccatin1  11299  swrdccatin2  11303  swrdccat3b  11314  caucvgre  11535  resqrexlemlo  11567  cau3lem  11668  qdenre  11756  rexico  11775  fimaxre2  11781  2zinfmin  11797  xrmaxiflemcl  11799  xrmaxifle  11800  xrmaxiflemcom  11803  2clim  11855  cn1lem  11868  climsqz  11889  climsqz2  11890  climcau  11901  sumrbdclem  11931  summodclem2a  11935  fsum3  11941  fsumcl2lem  11952  fsumadd  11960  sumsnf  11963  fsum2dlemstep  11988  fisum0diag2  12001  fsummulc2  12002  mertenslemub  12088  mertenslemi1  12089  mertensabs  12091  ntrivcvgap  12102  prodrbdclem  12125  prodmodclem3  12129  prodmodclem2a  12130  prodmodc  12132  prod1dc  12140  prodsnf  12146  fprod2dlemstep  12176  efaddlem  12228  tanaddaplem  12292  zdvdsdc  12366  dvdseq  12402  dvdsext  12409  odd2np1  12427  sqoddm1div8z  12440  nno  12460  dfgcd3  12574  nninfctlemfo  12604  dvdslcm  12634  lcmneg  12639  lcmgcdlem  12642  ncoprmgcdne1b  12654  qredeq  12661  qredeu  12662  divgcdcoprm0  12666  exprmfct  12703  prmdvdsfz  12704  isprm5  12707  rpexp1i  12719  sqrt2irr  12727  nonsq  12772  eulerthlemrprm  12794  eulerthlema  12795  phisum  12806  modprmn0modprm0  12822  pclemdc  12854  pcz  12898  pcmpt  12909  fldivp1  12914  pcfac  12916  expnprm  12919  oddprmdvds  12920  prmpwdvds  12921  infpnlem1  12925  1arith  12933  4sqlem2  12955  4sqlemafi  12961  4sqleminfi  12963  4sqexercise2  12965  4sqlemsdc  12966  ctinfom  13042  enctlem  13046  nninfdclemlt  13065  setsfun  13110  setsfun0  13111  setscom  13115  gsumfzval  13467  mndissubm  13551  resmhm  13563  resmhm2  13564  mhmco  13566  gsumfzz  13571  gsumwsubmcl  13572  gsumwmhm  13574  dfgrp2  13603  isgrpinv  13630  mulgval  13702  mulgnnp1  13710  mulgz  13730  grpissubg  13774  resghm  13840  qusecsub  13911  isrng  13940  lmodfopne  14333  dflidl2rng  14488  gsumfzfsumlemm  14594  mulgrhm2  14617  znidomb  14665  znunit  14666  psrbaglesuppg  14679  psrbagfi  14680  tgdom  14789  ssrest  14899  cnfval  14911  cnpfval  14912  cnpval  14915  iscnp3  14920  ssidcn  14927  cnpnei  14936  cnntr  14942  cncnp  14947  cnptopresti  14955  tx1cn  14986  upxp  14989  imasnopn  15016  bdmet  15219  metcnp  15229  ivthinclemlr  15354  ivthinclemur  15356  ivthinc  15360  dvrecap  15430  dvmptfsum  15442  elply2  15452  plymullem1  15465  plycolemc  15475  plycjlemc  15477  dvply1  15482  pilem3  15500  relogeftb  15582  logbgcd1irr  15684  mpodvdsmulf1o  15707  mersenne  15714  lgslem4  15725  lgsval  15726  lgsfvalg  15727  lgsval2lem  15732  lgsmod  15748  lgsdir2lem4  15753  lgsdinn0  15770  lgsquad2lem2  15804  lgsquad3  15806  2lgslem1c  15812  2sqlem6  15842  2sqlem7  15843  isupgren  15939  wrdupgren  15940  isumgren  15949  wrdumgren  15950  isuspgren  16001  isusgren  16002  clwwlkext2edg  16231  clwwlknonex2  16248  2omap  16544  pw1map  16546  nnsf  16557  peano4nninf  16558  nninfalllem1  16560  nninfsellemqall  16567  nninfsellemeqinf  16568  nninffeq  16572  exmidsbthrlem  16576  isomninnlem  16584  iswomninnlem  16603  iswomni0  16605  ismkvnnlem  16606