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  4563  en2lp  4591  foun  5526  f1oprg  5551  fcof1o  5839  foeqcnvco  5840  f1eqcocnv  5841  caovord3  6101  f1o2ndf1  6295  smores2  6361  frecrdg  6475  nnaordex  6595  xpdom2  6899  xpen  6915  mapen  6916  xpmapenlem  6919  nndomo  6934  phpm  6935  fidifsnen  6940  isinfinf  6967  finexdc  6972  fientri3  6985  fiintim  7001  xpfi  7002  f1dmvrnfibi  7019  sbthlemi8  7039  djudom  7168  omp1eomlem  7169  difinfsn  7175  ctmlemr  7183  ctssdccl  7186  nnnninfeq  7203  enomnilem  7213  finomni  7215  ismkvnex  7230  enmkvlem  7236  nninfwlpoimlemginf  7251  exmidfodomrlemrALT  7284  exmidontriim  7310  netap  7339  exmidapne  7345  acnccim  7357  dfplpq2  7440  recclnq  7478  subhalfnqq  7500  distrnq0  7545  prarloclem3step  7582  genpml  7603  genpmu  7604  addnqprl  7615  addnqpru  7616  appdivnq  7649  mulnqprl  7654  mulnqpru  7655  mullocpr  7657  ltexprlemfl  7695  ltexprlemfu  7697  ltmprr  7728  archpr  7729  cauappcvgprlemm  7731  caucvgprlemladdrl  7764  caucvgprprlemopl  7783  caucvgprprlemopu  7785  recexgt0sr  7859  mulgt0sr  7864  elrealeu  7915  axcaucvglemcau  7984  axcaucvglemres  7985  cnegex  8223  apirr  8651  mulge0  8665  lemul12a  8908  lediv2a  8941  creur  9005  nndiv  9050  zaddcllemneg  9384  peano5uzti  9453  supinfneg  9688  infsupneg  9689  divfnzn  9714  xrltso  9890  xpncan  9965  xltadd1  9970  xleaddadd  9981  elioc2  10030  elico2  10031  elicc2  10032  exfzdc  10335  zsupcllemstep  10338  infssuzex  10342  suprzubdc  10345  exbtwnzlemex  10358  rebtwn2z  10363  modqid  10460  modqcyc  10470  mulqaddmodid  10475  modqadd2mod  10485  addmodlteq  10509  frecuzrdgg  10527  nninfinf  10554  seq3val  10571  seqvalcd  10572  seq3clss  10582  iseqf1olemqcl  10610  iseqf1olemnab  10612  seq3f1olemp  10626  seq3f1o  10628  seqf1oglem1  10630  seqfeq4g  10642  fser0const  10646  ser3ge0  10647  exp3vallem  10651  qsqeqor  10761  facndiv  10850  faclbnd  10852  bcval5  10874  hashen  10895  fihashdom  10914  hashunlem  10915  hashfacen  10947  zfz1isolemiso  10950  seq3coll  10953  caucvgre  11165  resqrexlemlo  11197  cau3lem  11298  qdenre  11386  rexico  11405  fimaxre2  11411  2zinfmin  11427  xrmaxiflemcl  11429  xrmaxifle  11430  xrmaxiflemcom  11433  2clim  11485  cn1lem  11498  climsqz  11519  climsqz2  11520  climcau  11531  sumrbdclem  11561  summodclem2a  11565  fsum3  11571  fsumcl2lem  11582  fsumadd  11590  sumsnf  11593  fsum2dlemstep  11618  fisum0diag2  11631  fsummulc2  11632  mertenslemub  11718  mertenslemi1  11719  mertensabs  11721  ntrivcvgap  11732  prodrbdclem  11755  prodmodclem3  11759  prodmodclem2a  11760  prodmodc  11762  prod1dc  11770  prodsnf  11776  fprod2dlemstep  11806  efaddlem  11858  tanaddaplem  11922  zdvdsdc  11996  dvdseq  12032  dvdsext  12039  odd2np1  12057  sqoddm1div8z  12070  nno  12090  dfgcd3  12204  nninfctlemfo  12234  dvdslcm  12264  lcmneg  12269  lcmgcdlem  12272  ncoprmgcdne1b  12284  qredeq  12291  qredeu  12292  divgcdcoprm0  12296  exprmfct  12333  prmdvdsfz  12334  isprm5  12337  rpexp1i  12349  sqrt2irr  12357  nonsq  12402  eulerthlemrprm  12424  eulerthlema  12425  phisum  12436  modprmn0modprm0  12452  pclemdc  12484  pcz  12528  pcmpt  12539  fldivp1  12544  pcfac  12546  expnprm  12549  oddprmdvds  12550  prmpwdvds  12551  infpnlem1  12555  1arith  12563  4sqlem2  12585  4sqlemafi  12591  4sqleminfi  12593  4sqexercise2  12595  4sqlemsdc  12596  ctinfom  12672  enctlem  12676  nninfdclemlt  12695  setsfun  12740  setsfun0  12741  setscom  12745  gsumfzval  13095  mndissubm  13179  resmhm  13191  resmhm2  13192  mhmco  13194  gsumfzz  13199  gsumwsubmcl  13200  gsumwmhm  13202  dfgrp2  13231  isgrpinv  13258  mulgval  13330  mulgnnp1  13338  mulgz  13358  grpissubg  13402  resghm  13468  qusecsub  13539  isrng  13568  lmodfopne  13960  dflidl2rng  14115  gsumfzfsumlemm  14221  mulgrhm2  14244  znidomb  14292  znunit  14293  psrbaglesuppg  14306  psrbagfi  14307  tgdom  14416  ssrest  14526  cnfval  14538  cnpfval  14539  cnpval  14542  iscnp3  14547  ssidcn  14554  cnpnei  14563  cnntr  14569  cncnp  14574  cnptopresti  14582  tx1cn  14613  upxp  14616  imasnopn  14643  bdmet  14846  metcnp  14856  ivthinclemlr  14981  ivthinclemur  14983  ivthinc  14987  dvrecap  15057  dvmptfsum  15069  elply2  15079  plymullem1  15092  plycolemc  15102  plycjlemc  15104  dvply1  15109  pilem3  15127  relogeftb  15209  logbgcd1irr  15311  mpodvdsmulf1o  15334  mersenne  15341  lgslem4  15352  lgsval  15353  lgsfvalg  15354  lgsval2lem  15359  lgsmod  15375  lgsdir2lem4  15380  lgsdinn0  15397  lgsquad2lem2  15431  lgsquad3  15433  2lgslem1c  15439  2sqlem6  15469  2sqlem7  15470  2omap  15750  nnsf  15760  peano4nninf  15761  nninfalllem1  15763  nninfsellemqall  15770  nninfsellemeqinf  15771  nninffeq  15775  exmidsbthrlem  15779  isomninnlem  15787  iswomninnlem  15806  iswomni0  15808  ismkvnnlem  15809