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  4595  en2lp  4623  foun  5567  f1oprg  5593  fcof1o  5886  foeqcnvco  5887  f1eqcocnv  5888  caovord3  6150  f1o2ndf1  6344  smores2  6410  frecrdg  6524  nnaordex  6644  xpdom2  6958  xpen  6974  mapen  6975  xpmapenlem  6978  nndomo  6993  phpm  6995  fidifsnen  7000  isinfinf  7027  finexdc  7032  fientri3  7045  fiintim  7061  xpfi  7062  f1dmvrnfibi  7079  sbthlemi8  7099  djudom  7228  omp1eomlem  7229  difinfsn  7235  ctmlemr  7243  ctssdccl  7246  nnnninfeq  7263  enomnilem  7273  finomni  7275  ismkvnex  7290  enmkvlem  7296  nninfwlpoimlemginf  7311  exmidfodomrlemrALT  7349  exmidontriim  7375  netap  7408  exmidapne  7414  acnccim  7426  dfplpq2  7509  recclnq  7547  subhalfnqq  7569  distrnq0  7614  prarloclem3step  7651  genpml  7672  genpmu  7673  addnqprl  7684  addnqpru  7685  appdivnq  7718  mulnqprl  7723  mulnqpru  7724  mullocpr  7726  ltexprlemfl  7764  ltexprlemfu  7766  ltmprr  7797  archpr  7798  cauappcvgprlemm  7800  caucvgprlemladdrl  7833  caucvgprprlemopl  7852  caucvgprprlemopu  7854  recexgt0sr  7928  mulgt0sr  7933  elrealeu  7984  axcaucvglemcau  8053  axcaucvglemres  8054  cnegex  8292  apirr  8720  mulge0  8734  lemul12a  8977  lediv2a  9010  creur  9074  nndiv  9119  zaddcllemneg  9453  peano5uzti  9523  supinfneg  9758  infsupneg  9759  divfnzn  9784  xrltso  9960  xpncan  10035  xltadd1  10040  xleaddadd  10051  elioc2  10100  elico2  10101  elicc2  10102  exfzdc  10413  zsupcllemstep  10416  infssuzex  10420  suprzubdc  10423  exbtwnzlemex  10436  rebtwn2z  10441  modqid  10538  modqcyc  10548  mulqaddmodid  10553  modqadd2mod  10563  addmodlteq  10587  frecuzrdgg  10605  nninfinf  10632  seq3val  10649  seqvalcd  10650  seq3clss  10660  iseqf1olemqcl  10688  iseqf1olemnab  10690  seq3f1olemp  10704  seq3f1o  10706  seqf1oglem1  10708  seqfeq4g  10720  fser0const  10724  ser3ge0  10725  exp3vallem  10729  qsqeqor  10839  facndiv  10928  faclbnd  10930  bcval5  10952  hashen  10973  fihashdom  10992  hashunlem  10993  hashfacen  11025  zfz1isolemiso  11028  seq3coll  11031  ccatsymb  11103  ccatrn  11110  ccatw2s1p2  11142  swrdccatin1  11223  swrdccatin2  11227  swrdccat3b  11238  caucvgre  11458  resqrexlemlo  11490  cau3lem  11591  qdenre  11679  rexico  11698  fimaxre2  11704  2zinfmin  11720  xrmaxiflemcl  11722  xrmaxifle  11723  xrmaxiflemcom  11726  2clim  11778  cn1lem  11791  climsqz  11812  climsqz2  11813  climcau  11824  sumrbdclem  11854  summodclem2a  11858  fsum3  11864  fsumcl2lem  11875  fsumadd  11883  sumsnf  11886  fsum2dlemstep  11911  fisum0diag2  11924  fsummulc2  11925  mertenslemub  12011  mertenslemi1  12012  mertensabs  12014  ntrivcvgap  12025  prodrbdclem  12048  prodmodclem3  12052  prodmodclem2a  12053  prodmodc  12055  prod1dc  12063  prodsnf  12069  fprod2dlemstep  12099  efaddlem  12151  tanaddaplem  12215  zdvdsdc  12289  dvdseq  12325  dvdsext  12332  odd2np1  12350  sqoddm1div8z  12363  nno  12383  dfgcd3  12497  nninfctlemfo  12527  dvdslcm  12557  lcmneg  12562  lcmgcdlem  12565  ncoprmgcdne1b  12577  qredeq  12584  qredeu  12585  divgcdcoprm0  12589  exprmfct  12626  prmdvdsfz  12627  isprm5  12630  rpexp1i  12642  sqrt2irr  12650  nonsq  12695  eulerthlemrprm  12717  eulerthlema  12718  phisum  12729  modprmn0modprm0  12745  pclemdc  12777  pcz  12821  pcmpt  12832  fldivp1  12837  pcfac  12839  expnprm  12842  oddprmdvds  12843  prmpwdvds  12844  infpnlem1  12848  1arith  12856  4sqlem2  12878  4sqlemafi  12884  4sqleminfi  12886  4sqexercise2  12888  4sqlemsdc  12889  ctinfom  12965  enctlem  12969  nninfdclemlt  12988  setsfun  13033  setsfun0  13034  setscom  13038  gsumfzval  13390  mndissubm  13474  resmhm  13486  resmhm2  13487  mhmco  13489  gsumfzz  13494  gsumwsubmcl  13495  gsumwmhm  13497  dfgrp2  13526  isgrpinv  13553  mulgval  13625  mulgnnp1  13633  mulgz  13653  grpissubg  13697  resghm  13763  qusecsub  13834  isrng  13863  lmodfopne  14255  dflidl2rng  14410  gsumfzfsumlemm  14516  mulgrhm2  14539  znidomb  14587  znunit  14588  psrbaglesuppg  14601  psrbagfi  14602  tgdom  14711  ssrest  14821  cnfval  14833  cnpfval  14834  cnpval  14837  iscnp3  14842  ssidcn  14849  cnpnei  14858  cnntr  14864  cncnp  14869  cnptopresti  14877  tx1cn  14908  upxp  14911  imasnopn  14938  bdmet  15141  metcnp  15151  ivthinclemlr  15276  ivthinclemur  15278  ivthinc  15282  dvrecap  15352  dvmptfsum  15364  elply2  15374  plymullem1  15387  plycolemc  15397  plycjlemc  15399  dvply1  15404  pilem3  15422  relogeftb  15504  logbgcd1irr  15606  mpodvdsmulf1o  15629  mersenne  15636  lgslem4  15647  lgsval  15648  lgsfvalg  15649  lgsval2lem  15654  lgsmod  15670  lgsdir2lem4  15675  lgsdinn0  15692  lgsquad2lem2  15726  lgsquad3  15728  2lgslem1c  15734  2sqlem6  15764  2sqlem7  15765  isupgren  15860  wrdupgren  15861  isumgren  15870  wrdumgren  15871  isuspgren  15920  isusgren  15921  2omap  16270  pw1map  16272  nnsf  16282  peano4nninf  16283  nninfalllem1  16285  nninfsellemqall  16292  nninfsellemeqinf  16293  nninffeq  16297  exmidsbthrlem  16301  isomninnlem  16309  iswomninnlem  16328  iswomni0  16330  ismkvnnlem  16331