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  4618  en2lp  4646  foun  5593  f1oprg  5619  fcof1o  5919  foeqcnvco  5920  f1eqcocnv  5921  caovord3  6185  f1o2ndf1  6380  smores2  6446  frecrdg  6560  nnaordex  6682  xpdom2  6998  xpen  7014  mapen  7015  xpmapenlem  7018  nndomo  7033  phpm  7035  fidifsnen  7040  isinfinf  7067  finexdc  7072  fientri3  7085  fiintim  7101  xpfi  7102  f1dmvrnfibi  7119  sbthlemi8  7139  djudom  7268  omp1eomlem  7269  difinfsn  7275  ctmlemr  7283  ctssdccl  7286  nnnninfeq  7303  enomnilem  7313  finomni  7315  ismkvnex  7330  enmkvlem  7336  nninfwlpoimlemginf  7351  exmidfodomrlemrALT  7389  exmidontriim  7415  netap  7448  exmidapne  7454  acnccim  7466  dfplpq2  7549  recclnq  7587  subhalfnqq  7609  distrnq0  7654  prarloclem3step  7691  genpml  7712  genpmu  7713  addnqprl  7724  addnqpru  7725  appdivnq  7758  mulnqprl  7763  mulnqpru  7764  mullocpr  7766  ltexprlemfl  7804  ltexprlemfu  7806  ltmprr  7837  archpr  7838  cauappcvgprlemm  7840  caucvgprlemladdrl  7873  caucvgprprlemopl  7892  caucvgprprlemopu  7894  recexgt0sr  7968  mulgt0sr  7973  elrealeu  8024  axcaucvglemcau  8093  axcaucvglemres  8094  cnegex  8332  apirr  8760  mulge0  8774  lemul12a  9017  lediv2a  9050  creur  9114  nndiv  9159  zaddcllemneg  9493  peano5uzti  9563  supinfneg  9798  infsupneg  9799  divfnzn  9824  xrltso  10000  xpncan  10075  xltadd1  10080  xleaddadd  10091  elioc2  10140  elico2  10141  elicc2  10142  exfzdc  10454  zsupcllemstep  10457  infssuzex  10461  suprzubdc  10464  exbtwnzlemex  10477  rebtwn2z  10482  modqid  10579  modqcyc  10589  mulqaddmodid  10594  modqadd2mod  10604  addmodlteq  10628  frecuzrdgg  10646  nninfinf  10673  seq3val  10690  seqvalcd  10691  seq3clss  10701  iseqf1olemqcl  10729  iseqf1olemnab  10731  seq3f1olemp  10745  seq3f1o  10747  seqf1oglem1  10749  seqfeq4g  10761  fser0const  10765  ser3ge0  10766  exp3vallem  10770  qsqeqor  10880  facndiv  10969  faclbnd  10971  bcval5  10993  hashen  11014  fihashdom  11033  hashunlem  11034  hashfacen  11066  zfz1isolemiso  11069  seq3coll  11072  ccatsymb  11145  ccatrn  11152  ccatw2s1p2  11184  swrdccatin1  11265  swrdccatin2  11269  swrdccat3b  11280  caucvgre  11500  resqrexlemlo  11532  cau3lem  11633  qdenre  11721  rexico  11740  fimaxre2  11746  2zinfmin  11762  xrmaxiflemcl  11764  xrmaxifle  11765  xrmaxiflemcom  11768  2clim  11820  cn1lem  11833  climsqz  11854  climsqz2  11855  climcau  11866  sumrbdclem  11896  summodclem2a  11900  fsum3  11906  fsumcl2lem  11917  fsumadd  11925  sumsnf  11928  fsum2dlemstep  11953  fisum0diag2  11966  fsummulc2  11967  mertenslemub  12053  mertenslemi1  12054  mertensabs  12056  ntrivcvgap  12067  prodrbdclem  12090  prodmodclem3  12094  prodmodclem2a  12095  prodmodc  12097  prod1dc  12105  prodsnf  12111  fprod2dlemstep  12141  efaddlem  12193  tanaddaplem  12257  zdvdsdc  12331  dvdseq  12367  dvdsext  12374  odd2np1  12392  sqoddm1div8z  12405  nno  12425  dfgcd3  12539  nninfctlemfo  12569  dvdslcm  12599  lcmneg  12604  lcmgcdlem  12607  ncoprmgcdne1b  12619  qredeq  12626  qredeu  12627  divgcdcoprm0  12631  exprmfct  12668  prmdvdsfz  12669  isprm5  12672  rpexp1i  12684  sqrt2irr  12692  nonsq  12737  eulerthlemrprm  12759  eulerthlema  12760  phisum  12771  modprmn0modprm0  12787  pclemdc  12819  pcz  12863  pcmpt  12874  fldivp1  12879  pcfac  12881  expnprm  12884  oddprmdvds  12885  prmpwdvds  12886  infpnlem1  12890  1arith  12898  4sqlem2  12920  4sqlemafi  12926  4sqleminfi  12928  4sqexercise2  12930  4sqlemsdc  12931  ctinfom  13007  enctlem  13011  nninfdclemlt  13030  setsfun  13075  setsfun0  13076  setscom  13080  gsumfzval  13432  mndissubm  13516  resmhm  13528  resmhm2  13529  mhmco  13531  gsumfzz  13536  gsumwsubmcl  13537  gsumwmhm  13539  dfgrp2  13568  isgrpinv  13595  mulgval  13667  mulgnnp1  13675  mulgz  13695  grpissubg  13739  resghm  13805  qusecsub  13876  isrng  13905  lmodfopne  14298  dflidl2rng  14453  gsumfzfsumlemm  14559  mulgrhm2  14582  znidomb  14630  znunit  14631  psrbaglesuppg  14644  psrbagfi  14645  tgdom  14754  ssrest  14864  cnfval  14876  cnpfval  14877  cnpval  14880  iscnp3  14885  ssidcn  14892  cnpnei  14901  cnntr  14907  cncnp  14912  cnptopresti  14920  tx1cn  14951  upxp  14954  imasnopn  14981  bdmet  15184  metcnp  15194  ivthinclemlr  15319  ivthinclemur  15321  ivthinc  15325  dvrecap  15395  dvmptfsum  15407  elply2  15417  plymullem1  15430  plycolemc  15440  plycjlemc  15442  dvply1  15447  pilem3  15465  relogeftb  15547  logbgcd1irr  15649  mpodvdsmulf1o  15672  mersenne  15679  lgslem4  15690  lgsval  15691  lgsfvalg  15692  lgsval2lem  15697  lgsmod  15713  lgsdir2lem4  15718  lgsdinn0  15735  lgsquad2lem2  15769  lgsquad3  15771  2lgslem1c  15777  2sqlem6  15807  2sqlem7  15808  isupgren  15903  wrdupgren  15904  isumgren  15913  wrdumgren  15914  isuspgren  15963  isusgren  15964  fidcen  16379  2omap  16388  pw1map  16390  nnsf  16401  peano4nninf  16402  nninfalllem1  16404  nninfsellemqall  16411  nninfsellemeqinf  16412  nninffeq  16416  exmidsbthrlem  16420  isomninnlem  16428  iswomninnlem  16447  iswomni0  16449  ismkvnnlem  16450