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  4559  en2lp  4587  foun  5520  f1oprg  5545  fcof1o  5833  foeqcnvco  5834  f1eqcocnv  5835  caovord3  6094  f1o2ndf1  6283  smores2  6349  frecrdg  6463  nnaordex  6583  xpdom2  6887  xpen  6903  mapen  6904  xpmapenlem  6907  nndomo  6922  phpm  6923  fidifsnen  6928  isinfinf  6955  finexdc  6960  fientri3  6973  fiintim  6987  xpfi  6988  f1dmvrnfibi  7005  sbthlemi8  7025  djudom  7154  omp1eomlem  7155  difinfsn  7161  ctmlemr  7169  ctssdccl  7172  nnnninfeq  7189  enomnilem  7199  finomni  7201  ismkvnex  7216  enmkvlem  7222  nninfwlpoimlemginf  7237  exmidfodomrlemrALT  7265  exmidontriim  7287  netap  7316  exmidapne  7322  dfplpq2  7416  recclnq  7454  subhalfnqq  7476  distrnq0  7521  prarloclem3step  7558  genpml  7579  genpmu  7580  addnqprl  7591  addnqpru  7592  appdivnq  7625  mulnqprl  7630  mulnqpru  7631  mullocpr  7633  ltexprlemfl  7671  ltexprlemfu  7673  ltmprr  7704  archpr  7705  cauappcvgprlemm  7707  caucvgprlemladdrl  7740  caucvgprprlemopl  7759  caucvgprprlemopu  7761  recexgt0sr  7835  mulgt0sr  7840  elrealeu  7891  axcaucvglemcau  7960  axcaucvglemres  7961  cnegex  8199  apirr  8626  mulge0  8640  lemul12a  8883  lediv2a  8916  creur  8980  nndiv  9025  zaddcllemneg  9359  peano5uzti  9428  supinfneg  9663  infsupneg  9664  divfnzn  9689  xrltso  9865  xpncan  9940  xltadd1  9945  xleaddadd  9956  elioc2  10005  elico2  10006  elicc2  10007  exfzdc  10310  exbtwnzlemex  10321  rebtwn2z  10326  modqid  10423  modqcyc  10433  mulqaddmodid  10438  modqadd2mod  10448  addmodlteq  10472  frecuzrdgg  10490  nninfinf  10517  seq3val  10534  seqvalcd  10535  seq3clss  10545  iseqf1olemqcl  10573  iseqf1olemnab  10575  seq3f1olemp  10589  seq3f1o  10591  seqf1oglem1  10593  seqfeq4g  10605  fser0const  10609  ser3ge0  10610  exp3vallem  10614  qsqeqor  10724  facndiv  10813  faclbnd  10815  bcval5  10837  hashen  10858  fihashdom  10877  hashunlem  10878  hashfacen  10910  zfz1isolemiso  10913  seq3coll  10916  caucvgre  11128  resqrexlemlo  11160  cau3lem  11261  qdenre  11349  rexico  11368  fimaxre2  11373  2zinfmin  11389  xrmaxiflemcl  11391  xrmaxifle  11392  xrmaxiflemcom  11395  2clim  11447  cn1lem  11460  climsqz  11481  climsqz2  11482  climcau  11493  sumrbdclem  11523  summodclem2a  11527  fsum3  11533  fsumcl2lem  11544  fsumadd  11552  sumsnf  11555  fsum2dlemstep  11580  fisum0diag2  11593  fsummulc2  11594  mertenslemub  11680  mertenslemi1  11681  mertensabs  11683  ntrivcvgap  11694  prodrbdclem  11717  prodmodclem3  11721  prodmodclem2a  11722  prodmodc  11724  prod1dc  11732  prodsnf  11738  fprod2dlemstep  11768  efaddlem  11820  tanaddaplem  11884  zdvdsdc  11958  dvdseq  11993  dvdsext  12000  odd2np1  12017  sqoddm1div8z  12030  nno  12050  zsupcllemstep  12085  infssuzex  12089  suprzubdc  12092  dfgcd3  12150  nninfctlemfo  12180  dvdslcm  12210  lcmneg  12215  lcmgcdlem  12218  ncoprmgcdne1b  12230  qredeq  12237  qredeu  12238  divgcdcoprm0  12242  exprmfct  12279  prmdvdsfz  12280  isprm5  12283  rpexp1i  12295  sqrt2irr  12303  nonsq  12348  eulerthlemrprm  12370  eulerthlema  12371  phisum  12381  modprmn0modprm0  12397  pclemdc  12429  pcz  12473  pcmpt  12484  fldivp1  12489  pcfac  12491  expnprm  12494  oddprmdvds  12495  prmpwdvds  12496  infpnlem1  12500  1arith  12508  4sqlem2  12530  4sqlemafi  12536  4sqleminfi  12538  4sqexercise2  12540  4sqlemsdc  12541  ctinfom  12588  enctlem  12592  nninfdclemlt  12611  setsfun  12656  setsfun0  12657  setscom  12661  gsumfzval  12977  mndissubm  13050  resmhm  13062  resmhm2  13063  mhmco  13065  gsumfzz  13070  gsumwsubmcl  13071  gsumwmhm  13073  dfgrp2  13102  isgrpinv  13129  mulgval  13195  mulgnnp1  13203  mulgz  13223  grpissubg  13267  resghm  13333  qusecsub  13404  isrng  13433  lmodfopne  13825  dflidl2rng  13980  gsumfzfsumlemm  14086  mulgrhm2  14109  znidomb  14157  znunit  14158  psrbaglesuppg  14169  tgdom  14251  ssrest  14361  cnfval  14373  cnpfval  14374  cnpval  14377  iscnp3  14382  ssidcn  14389  cnpnei  14398  cnntr  14404  cncnp  14409  cnptopresti  14417  tx1cn  14448  upxp  14451  imasnopn  14478  bdmet  14681  metcnp  14691  ivthinclemlr  14816  ivthinclemur  14818  ivthinc  14822  dvrecap  14892  dvmptfsum  14904  elply2  14914  plymullem1  14927  plycolemc  14936  plycjlemc  14938  dvply1  14943  pilem3  14959  relogeftb  15041  logbgcd1irr  15140  lgslem4  15160  lgsval  15161  lgsfvalg  15162  lgsval2lem  15167  lgsmod  15183  lgsdir2lem4  15188  lgsdinn0  15205  lgsquad2lem2  15239  lgsquad3  15241  2lgslem1c  15247  2sqlem6  15277  2sqlem7  15278  nnsf  15565  peano4nninf  15566  nninfalllem1  15568  nninfsellemqall  15575  nninfsellemeqinf  15576  nninffeq  15580  exmidsbthrlem  15582  isomninnlem  15590  iswomninnlem  15609  iswomni0  15611  ismkvnnlem  15612