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  4526  en2lp  4554  foun  5481  f1oprg  5506  fcof1o  5790  foeqcnvco  5791  f1eqcocnv  5792  caovord3  6048  f1o2ndf1  6229  smores2  6295  frecrdg  6409  nnaordex  6529  xpdom2  6831  xpen  6845  mapen  6846  xpmapenlem  6849  nndomo  6864  phpm  6865  fidifsnen  6870  isinfinf  6897  finexdc  6902  fientri3  6914  fiintim  6928  xpfi  6929  f1dmvrnfibi  6943  sbthlemi8  6963  djudom  7092  omp1eomlem  7093  difinfsn  7099  ctmlemr  7107  ctssdccl  7110  nnnninfeq  7126  enomnilem  7136  finomni  7138  ismkvnex  7153  enmkvlem  7159  nninfwlpoimlemginf  7174  exmidfodomrlemrALT  7202  exmidontriim  7224  netap  7253  exmidapne  7259  dfplpq2  7353  recclnq  7391  subhalfnqq  7413  distrnq0  7458  prarloclem3step  7495  genpml  7516  genpmu  7517  addnqprl  7528  addnqpru  7529  appdivnq  7562  mulnqprl  7567  mulnqpru  7568  mullocpr  7570  ltexprlemfl  7608  ltexprlemfu  7610  ltmprr  7641  archpr  7642  cauappcvgprlemm  7644  caucvgprlemladdrl  7677  caucvgprprlemopl  7696  caucvgprprlemopu  7698  recexgt0sr  7772  mulgt0sr  7777  elrealeu  7828  axcaucvglemcau  7897  axcaucvglemres  7898  cnegex  8135  apirr  8562  mulge0  8576  lemul12a  8819  lediv2a  8852  creur  8916  nndiv  8960  zaddcllemneg  9292  peano5uzti  9361  supinfneg  9595  infsupneg  9596  divfnzn  9621  xrltso  9796  xpncan  9871  xltadd1  9876  xleaddadd  9887  elioc2  9936  elico2  9937  elicc2  9938  exfzdc  10240  exbtwnzlemex  10250  rebtwn2z  10255  modqid  10349  modqcyc  10359  mulqaddmodid  10364  modqadd2mod  10374  addmodlteq  10398  frecuzrdgg  10416  seq3val  10458  seqvalcd  10459  seq3clss  10467  iseqf1olemqcl  10486  iseqf1olemnab  10488  seq3f1olemp  10502  seq3f1o  10504  fser0const  10516  ser3ge0  10517  exp3vallem  10521  qsqeqor  10631  facndiv  10719  faclbnd  10721  bcval5  10743  hashen  10764  fihashdom  10783  hashunlem  10784  hashfacen  10816  zfz1isolemiso  10819  seq3coll  10822  caucvgre  10990  resqrexlemlo  11022  cau3lem  11123  qdenre  11211  rexico  11230  fimaxre2  11235  2zinfmin  11251  xrmaxiflemcl  11253  xrmaxifle  11254  xrmaxiflemcom  11257  2clim  11309  cn1lem  11322  climsqz  11343  climsqz2  11344  climcau  11355  sumrbdclem  11385  summodclem2a  11389  fsum3  11395  fsumcl2lem  11406  fsumadd  11414  sumsnf  11417  fsum2dlemstep  11442  fisum0diag2  11455  fsummulc2  11456  mertenslemub  11542  mertenslemi1  11543  mertensabs  11545  ntrivcvgap  11556  prodrbdclem  11579  prodmodclem3  11583  prodmodclem2a  11584  prodmodc  11586  prod1dc  11594  prodsnf  11600  fprod2dlemstep  11630  efaddlem  11682  tanaddaplem  11746  zdvdsdc  11819  dvdseq  11854  dvdsext  11861  odd2np1  11878  sqoddm1div8z  11891  nno  11911  zsupcllemstep  11946  infssuzex  11950  suprzubdc  11953  dfgcd3  12011  dvdslcm  12069  lcmneg  12074  lcmgcdlem  12077  ncoprmgcdne1b  12089  qredeq  12096  qredeu  12097  divgcdcoprm0  12101  exprmfct  12138  prmdvdsfz  12139  isprm5  12142  rpexp1i  12154  sqrt2irr  12162  nonsq  12207  eulerthlemrprm  12229  eulerthlema  12230  phisum  12240  modprmn0modprm0  12256  pclemdc  12288  pcz  12331  pcmpt  12341  fldivp1  12346  pcfac  12348  expnprm  12351  oddprmdvds  12352  prmpwdvds  12353  infpnlem1  12357  1arith  12365  4sqlem2  12387  ctinfom  12429  enctlem  12433  nninfdclemlt  12452  setsfun  12497  setsfun0  12498  setscom  12502  mndissubm  12866  mhmco  12874  dfgrp2  12902  isgrpinv  12926  mulgval  12986  mulgnnp1  12991  mulgz  13011  grpissubg  13054  lmodfopne  13416  tgdom  13575  ssrest  13685  cnfval  13697  cnpfval  13698  cnpval  13701  iscnp3  13706  ssidcn  13713  cnpnei  13722  cnntr  13728  cncnp  13733  cnptopresti  13741  tx1cn  13772  upxp  13775  imasnopn  13802  bdmet  14005  metcnp  14015  ivthinclemlr  14118  ivthinclemur  14120  ivthinc  14124  dvrecap  14180  pilem3  14207  relogeftb  14289  logbgcd1irr  14388  lgslem4  14407  lgsval  14408  lgsfvalg  14409  lgsval2lem  14414  lgsmod  14430  lgsdir2lem4  14435  lgsdinn0  14452  2sqlem6  14470  2sqlem7  14471  nnsf  14757  peano4nninf  14758  nninfalllem1  14760  nninfsellemqall  14767  nninfsellemeqinf  14768  nninffeq  14772  exmidsbthrlem  14773  isomninnlem  14781  iswomninnlem  14800  iswomni0  14802  ismkvnnlem  14803