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  4619  en2lp  4647  foun  5596  f1oprg  5622  fcof1o  5922  foeqcnvco  5923  f1eqcocnv  5924  caovord3  6188  f1o2ndf1  6385  smores2  6451  frecrdg  6565  nnaordex  6687  xpdom2  7003  xpen  7019  mapen  7020  xpmapenlem  7023  nndomo  7038  phpm  7040  fidifsnen  7045  isinfinf  7072  fidcen  7074  finexdc  7078  elssdc  7080  fientri3  7093  fiintim  7109  xpfi  7110  f1dmvrnfibi  7127  sbthlemi8  7147  djudom  7276  omp1eomlem  7277  difinfsn  7283  ctmlemr  7291  ctssdccl  7294  nnnninfeq  7311  enomnilem  7321  finomni  7323  ismkvnex  7338  enmkvlem  7344  nninfwlpoimlemginf  7359  exmidfodomrlemrALT  7397  exmidontriim  7423  netap  7456  exmidapne  7462  acnccim  7474  dfplpq2  7557  recclnq  7595  subhalfnqq  7617  distrnq0  7662  prarloclem3step  7699  genpml  7720  genpmu  7721  addnqprl  7732  addnqpru  7733  appdivnq  7766  mulnqprl  7771  mulnqpru  7772  mullocpr  7774  ltexprlemfl  7812  ltexprlemfu  7814  ltmprr  7845  archpr  7846  cauappcvgprlemm  7848  caucvgprlemladdrl  7881  caucvgprprlemopl  7900  caucvgprprlemopu  7902  recexgt0sr  7976  mulgt0sr  7981  elrealeu  8032  axcaucvglemcau  8101  axcaucvglemres  8102  cnegex  8340  apirr  8768  mulge0  8782  lemul12a  9025  lediv2a  9058  creur  9122  nndiv  9167  zaddcllemneg  9501  peano5uzti  9571  supinfneg  9807  infsupneg  9808  divfnzn  9833  xrltso  10009  xpncan  10084  xltadd1  10089  xleaddadd  10100  elioc2  10149  elico2  10150  elicc2  10151  exfzdc  10463  zsupcllemstep  10466  infssuzex  10470  suprzubdc  10473  exbtwnzlemex  10486  rebtwn2z  10491  modqid  10588  modqcyc  10598  mulqaddmodid  10603  modqadd2mod  10613  addmodlteq  10637  frecuzrdgg  10655  nninfinf  10682  seq3val  10699  seqvalcd  10700  seq3clss  10710  iseqf1olemqcl  10738  iseqf1olemnab  10740  seq3f1olemp  10754  seq3f1o  10756  seqf1oglem1  10758  seqfeq4g  10770  fser0const  10774  ser3ge0  10775  exp3vallem  10779  qsqeqor  10889  facndiv  10978  faclbnd  10980  bcval5  11002  hashen  11023  fihashdom  11042  hashunlem  11043  hashfacen  11076  zfz1isolemiso  11079  seq3coll  11082  ccatsymb  11155  ccatrn  11162  ccatw2s1p2  11197  swrdccatin1  11278  swrdccatin2  11282  swrdccat3b  11293  caucvgre  11513  resqrexlemlo  11545  cau3lem  11646  qdenre  11734  rexico  11753  fimaxre2  11759  2zinfmin  11775  xrmaxiflemcl  11777  xrmaxifle  11778  xrmaxiflemcom  11781  2clim  11833  cn1lem  11846  climsqz  11867  climsqz2  11868  climcau  11879  sumrbdclem  11909  summodclem2a  11913  fsum3  11919  fsumcl2lem  11930  fsumadd  11938  sumsnf  11941  fsum2dlemstep  11966  fisum0diag2  11979  fsummulc2  11980  mertenslemub  12066  mertenslemi1  12067  mertensabs  12069  ntrivcvgap  12080  prodrbdclem  12103  prodmodclem3  12107  prodmodclem2a  12108  prodmodc  12110  prod1dc  12118  prodsnf  12124  fprod2dlemstep  12154  efaddlem  12206  tanaddaplem  12270  zdvdsdc  12344  dvdseq  12380  dvdsext  12387  odd2np1  12405  sqoddm1div8z  12418  nno  12438  dfgcd3  12552  nninfctlemfo  12582  dvdslcm  12612  lcmneg  12617  lcmgcdlem  12620  ncoprmgcdne1b  12632  qredeq  12639  qredeu  12640  divgcdcoprm0  12644  exprmfct  12681  prmdvdsfz  12682  isprm5  12685  rpexp1i  12697  sqrt2irr  12705  nonsq  12750  eulerthlemrprm  12772  eulerthlema  12773  phisum  12784  modprmn0modprm0  12800  pclemdc  12832  pcz  12876  pcmpt  12887  fldivp1  12892  pcfac  12894  expnprm  12897  oddprmdvds  12898  prmpwdvds  12899  infpnlem1  12903  1arith  12911  4sqlem2  12933  4sqlemafi  12939  4sqleminfi  12941  4sqexercise2  12943  4sqlemsdc  12944  ctinfom  13020  enctlem  13024  nninfdclemlt  13043  setsfun  13088  setsfun0  13089  setscom  13093  gsumfzval  13445  mndissubm  13529  resmhm  13541  resmhm2  13542  mhmco  13544  gsumfzz  13549  gsumwsubmcl  13550  gsumwmhm  13552  dfgrp2  13581  isgrpinv  13608  mulgval  13680  mulgnnp1  13688  mulgz  13708  grpissubg  13752  resghm  13818  qusecsub  13889  isrng  13918  lmodfopne  14311  dflidl2rng  14466  gsumfzfsumlemm  14572  mulgrhm2  14595  znidomb  14643  znunit  14644  psrbaglesuppg  14657  psrbagfi  14658  tgdom  14767  ssrest  14877  cnfval  14889  cnpfval  14890  cnpval  14893  iscnp3  14898  ssidcn  14905  cnpnei  14914  cnntr  14920  cncnp  14925  cnptopresti  14933  tx1cn  14964  upxp  14967  imasnopn  14994  bdmet  15197  metcnp  15207  ivthinclemlr  15332  ivthinclemur  15334  ivthinc  15338  dvrecap  15408  dvmptfsum  15420  elply2  15430  plymullem1  15443  plycolemc  15453  plycjlemc  15455  dvply1  15460  pilem3  15478  relogeftb  15560  logbgcd1irr  15662  mpodvdsmulf1o  15685  mersenne  15692  lgslem4  15703  lgsval  15704  lgsfvalg  15705  lgsval2lem  15710  lgsmod  15726  lgsdir2lem4  15731  lgsdinn0  15748  lgsquad2lem2  15782  lgsquad3  15784  2lgslem1c  15790  2sqlem6  15820  2sqlem7  15821  isupgren  15916  wrdupgren  15917  isumgren  15926  wrdumgren  15927  isuspgren  15976  isusgren  15977  clwwlkext2edg  16190  2omap  16472  pw1map  16474  nnsf  16485  peano4nninf  16486  nninfalllem1  16488  nninfsellemqall  16495  nninfsellemeqinf  16496  nninffeq  16500  exmidsbthrlem  16504  isomninnlem  16512  iswomninnlem  16531  iswomni0  16533  ismkvnnlem  16534