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  4578  en2lp  4606  foun  5548  f1oprg  5573  fcof1o  5865  foeqcnvco  5866  f1eqcocnv  5867  caovord3  6127  f1o2ndf1  6321  smores2  6387  frecrdg  6501  nnaordex  6621  xpdom2  6933  xpen  6949  mapen  6950  xpmapenlem  6953  nndomo  6968  phpm  6969  fidifsnen  6974  isinfinf  7001  finexdc  7006  fientri3  7019  fiintim  7035  xpfi  7036  f1dmvrnfibi  7053  sbthlemi8  7073  djudom  7202  omp1eomlem  7203  difinfsn  7209  ctmlemr  7217  ctssdccl  7220  nnnninfeq  7237  enomnilem  7247  finomni  7249  ismkvnex  7264  enmkvlem  7270  nninfwlpoimlemginf  7285  exmidfodomrlemrALT  7318  exmidontriim  7344  netap  7373  exmidapne  7379  acnccim  7391  dfplpq2  7474  recclnq  7512  subhalfnqq  7534  distrnq0  7579  prarloclem3step  7616  genpml  7637  genpmu  7638  addnqprl  7649  addnqpru  7650  appdivnq  7683  mulnqprl  7688  mulnqpru  7689  mullocpr  7691  ltexprlemfl  7729  ltexprlemfu  7731  ltmprr  7762  archpr  7763  cauappcvgprlemm  7765  caucvgprlemladdrl  7798  caucvgprprlemopl  7817  caucvgprprlemopu  7819  recexgt0sr  7893  mulgt0sr  7898  elrealeu  7949  axcaucvglemcau  8018  axcaucvglemres  8019  cnegex  8257  apirr  8685  mulge0  8699  lemul12a  8942  lediv2a  8975  creur  9039  nndiv  9084  zaddcllemneg  9418  peano5uzti  9488  supinfneg  9723  infsupneg  9724  divfnzn  9749  xrltso  9925  xpncan  10000  xltadd1  10005  xleaddadd  10016  elioc2  10065  elico2  10066  elicc2  10067  exfzdc  10376  zsupcllemstep  10379  infssuzex  10383  suprzubdc  10386  exbtwnzlemex  10399  rebtwn2z  10404  modqid  10501  modqcyc  10511  mulqaddmodid  10516  modqadd2mod  10526  addmodlteq  10550  frecuzrdgg  10568  nninfinf  10595  seq3val  10612  seqvalcd  10613  seq3clss  10623  iseqf1olemqcl  10651  iseqf1olemnab  10653  seq3f1olemp  10667  seq3f1o  10669  seqf1oglem1  10671  seqfeq4g  10683  fser0const  10687  ser3ge0  10688  exp3vallem  10692  qsqeqor  10802  facndiv  10891  faclbnd  10893  bcval5  10915  hashen  10936  fihashdom  10955  hashunlem  10956  hashfacen  10988  zfz1isolemiso  10991  seq3coll  10994  ccatsymb  11066  ccatrn  11073  ccatw2s1p2  11105  caucvgre  11336  resqrexlemlo  11368  cau3lem  11469  qdenre  11557  rexico  11576  fimaxre2  11582  2zinfmin  11598  xrmaxiflemcl  11600  xrmaxifle  11601  xrmaxiflemcom  11604  2clim  11656  cn1lem  11669  climsqz  11690  climsqz2  11691  climcau  11702  sumrbdclem  11732  summodclem2a  11736  fsum3  11742  fsumcl2lem  11753  fsumadd  11761  sumsnf  11764  fsum2dlemstep  11789  fisum0diag2  11802  fsummulc2  11803  mertenslemub  11889  mertenslemi1  11890  mertensabs  11892  ntrivcvgap  11903  prodrbdclem  11926  prodmodclem3  11930  prodmodclem2a  11931  prodmodc  11933  prod1dc  11941  prodsnf  11947  fprod2dlemstep  11977  efaddlem  12029  tanaddaplem  12093  zdvdsdc  12167  dvdseq  12203  dvdsext  12210  odd2np1  12228  sqoddm1div8z  12241  nno  12261  dfgcd3  12375  nninfctlemfo  12405  dvdslcm  12435  lcmneg  12440  lcmgcdlem  12443  ncoprmgcdne1b  12455  qredeq  12462  qredeu  12463  divgcdcoprm0  12467  exprmfct  12504  prmdvdsfz  12505  isprm5  12508  rpexp1i  12520  sqrt2irr  12528  nonsq  12573  eulerthlemrprm  12595  eulerthlema  12596  phisum  12607  modprmn0modprm0  12623  pclemdc  12655  pcz  12699  pcmpt  12710  fldivp1  12715  pcfac  12717  expnprm  12720  oddprmdvds  12721  prmpwdvds  12722  infpnlem1  12726  1arith  12734  4sqlem2  12756  4sqlemafi  12762  4sqleminfi  12764  4sqexercise2  12766  4sqlemsdc  12767  ctinfom  12843  enctlem  12847  nninfdclemlt  12866  setsfun  12911  setsfun0  12912  setscom  12916  gsumfzval  13267  mndissubm  13351  resmhm  13363  resmhm2  13364  mhmco  13366  gsumfzz  13371  gsumwsubmcl  13372  gsumwmhm  13374  dfgrp2  13403  isgrpinv  13430  mulgval  13502  mulgnnp1  13510  mulgz  13530  grpissubg  13574  resghm  13640  qusecsub  13711  isrng  13740  lmodfopne  14132  dflidl2rng  14287  gsumfzfsumlemm  14393  mulgrhm2  14416  znidomb  14464  znunit  14465  psrbaglesuppg  14478  psrbagfi  14479  tgdom  14588  ssrest  14698  cnfval  14710  cnpfval  14711  cnpval  14714  iscnp3  14719  ssidcn  14726  cnpnei  14735  cnntr  14741  cncnp  14746  cnptopresti  14754  tx1cn  14785  upxp  14788  imasnopn  14815  bdmet  15018  metcnp  15028  ivthinclemlr  15153  ivthinclemur  15155  ivthinc  15159  dvrecap  15229  dvmptfsum  15241  elply2  15251  plymullem1  15264  plycolemc  15274  plycjlemc  15276  dvply1  15281  pilem3  15299  relogeftb  15381  logbgcd1irr  15483  mpodvdsmulf1o  15506  mersenne  15513  lgslem4  15524  lgsval  15525  lgsfvalg  15526  lgsval2lem  15531  lgsmod  15547  lgsdir2lem4  15552  lgsdinn0  15569  lgsquad2lem2  15603  lgsquad3  15605  2lgslem1c  15611  2sqlem6  15641  2sqlem7  15642  2omap  16006  nnsf  16016  peano4nninf  16017  nninfalllem1  16019  nninfsellemqall  16026  nninfsellemeqinf  16027  nninffeq  16031  exmidsbthrlem  16035  isomninnlem  16043  iswomninnlem  16062  iswomni0  16064  ismkvnnlem  16065