Theorem ad2antlr 493

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 480	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  497  simplr  533  simplrl  541  simplrr  542  ordtri2or2exmidlem  4671  en2lp  4699  foun  5656  f1oprg  5683  fcof1o  5989  foeqcnvco  5990  f1eqcocnv  5991  caovord3  6257  f1o2ndf1  6458  suppfnss  6491  suppssdc  6494  suppssfvg  6497  smores2  6559  frecrdg  6673  nnaordex  6795  xpdom2  7123  xpen  7139  mapen  7140  xpmapenlem  7143  nndomo  7159  phpm  7161  fidifsnen  7166  isinfinf  7195  fidcen  7197  finexdc  7201  elssdc  7203  fientri3  7216  fiintim  7232  xpfi  7233  f1dmvrnfibi  7252  sbthlemi8  7275  2omap  7312  2omapfi  7314  djudom  7427  omp1eomlem  7428  difinfsn  7434  ctmlemr  7442  ctssdccl  7445  nnnninfeq  7462  enomnilem  7472  finomni  7474  ismkvnex  7489  enmkvlem  7495  nninfwlpoimlemginf  7510  exmidfodomrlemrALT  7549  exmidontriim  7575  netap  7614  exmidapne  7620  acnccim  7632  dfplpq2  7715  recclnq  7753  subhalfnqq  7775  distrnq0  7820  prarloclem3step  7857  genpml  7878  genpmu  7879  addnqprl  7890  addnqpru  7891  appdivnq  7924  mulnqprl  7929  mulnqpru  7930  mullocpr  7932  ltexprlemfl  7970  ltexprlemfu  7972  ltmprr  8003  archpr  8004  cauappcvgprlemm  8006  caucvgprlemladdrl  8039  caucvgprprlemopl  8058  caucvgprprlemopu  8060  recexgt0sr  8134  mulgt0sr  8139  elrealeu  8190  axcaucvglemcau  8259  axcaucvglemres  8260  cnegex  8498  apirr  8927  mulge0  8941  lemul12a  9186  lediv2a  9219  creur  9283  nndiv  9328  zaddcllemneg  9666  peano5uzti  9737  supinfneg  9978  infsupneg  9979  divfnzn  10004  xrltso  10181  xpncan  10256  xltadd1  10261  xleaddadd  10272  elioc2  10321  elico2  10322  elicc2  10323  exfzdc  10642  zsupcllemstep  10645  infssuzex  10649  suprzubdc  10654  exbtwnzlemex  10667  rebtwn2z  10672  modqid  10769  modqcyc  10779  mulqaddmodid  10784  modqadd2mod  10794  addmodlteq  10818  frecuzrdgg  10836  nninfinf  10863  seq3val  10880  seqvalcd  10881  seq3clss  10891  iseqf1olemqcl  10919  iseqf1olemnab  10921  seq3f1olemp  10935  seq3f1o  10937  seqf1oglem1  10939  seqfeq4g  10951  fser0const  10955  ser3ge0  10956  exp3vallem  10960  qsqeqor  11070  facndiv  11160  faclbnd  11162  bcval5  11184  hashen  11206  fihashdom  11226  hashunlem  11227  hashfacen  11267  zfz1isolemiso  11274  seq3coll  11277  ccatsymb  11353  ccatrn  11360  ccatw2s1p2  11397  swrdccatin1  11480  swrdccatin2  11484  swrdccat3b  11495  caucvgre  11730  resqrexlemlo  11762  cau3lem  11863  qdenre  11951  rexico  11970  fimaxre2  11976  2zinfmin  11992  xrmaxiflemcl  11994  xrmaxifle  11995  xrmaxiflemcom  11998  2clim  12050  cn1lem  12063  climsqz  12084  climsqz2  12085  climcau  12096  sumrbdclem  12127  summodclem2a  12131  fsum3  12137  fsumcl2lem  12148  fsumadd  12156  sumsnf  12159  fsum2dlemstep  12184  fisum0diag2  12197  fsummulc2  12198  mertenslemub  12284  mertenslemi1  12285  mertensabs  12287  ntrivcvgap  12298  prodrbdclem  12321  prodmodclem3  12325  prodmodclem2a  12326  prodmodc  12328  prod1dc  12336  prodsnf  12342  fprod2dlemstep  12372  efaddlem  12424  tanaddaplem  12488  zdvdsdc  12562  dvdseq  12598  dvdsext  12605  odd2np1  12623  sqoddm1div8z  12636  nno  12656  dfgcd3  12770  nninfctlemfo  12800  dvdslcm  12830  lcmneg  12835  lcmgcdlem  12838  ncoprmgcdne1b  12850  qredeq  12857  qredeu  12858  divgcdcoprm0  12862  exprmfct  12899  prmdvdsfz  12900  isprm5  12903  rpexp1i  12915  sqrt2irr  12923  nonsq  12968  eulerthlemrprm  12990  eulerthlema  12991  phisum  13002  modprmn0modprm0  13018  pclemdc  13050  pcz  13094  pcmpt  13105  fldivp1  13110  pcfac  13112  expnprm  13115  oddprmdvds  13116  prmpwdvds  13117  infpnlem1  13121  1arith  13129  4sqlem2  13151  4sqlemafi  13157  4sqleminfi  13159  4sqexercise2  13161  4sqlemsdc  13162  ballotfilemsv  13236  ballotfilemsima  13242  ctinfom  13302  enctlem  13306  nninfdclemlt  13325  setsfun  13370  setsfun0  13371  setscom  13375  gzsumfzval  13694  mndissubm  13765  resmhm  13777  resmhm2  13778  mhmco  13780  gzsumwsubmcl  13784  gzsumwmhm  13786  dfgrp2  13815  isgrpinv  13842  mulgval  13908  mulgnnp1  13916  mulgz  13936  grpissubg  13980  resghm  14046  qusecsub  14118  gsumf1ofi  14143  isrng  14216  lmodfopne  14646  dflidl2rng  14801  mulgrhm2  14928  znidomb  14976  znunit  14977  issubassa2  15018  psrbaglesuppg  15040  psrbagfi  15042  tgdom  15156  ssrest  15266  cnfval  15278  cnpfval  15279  cnpval  15282  iscnp3  15287  ssidcn  15294  cnpnei  15303  cnntr  15309  cncnp  15314  cnptopresti  15322  tx1cn  15353  upxp  15356  imasnopn  15383  bdmet  15586  metcnp  15596  ivthinclemlr  15721  ivthinclemur  15723  ivthinc  15727  dvrecap  15797  dvmptfsum  15809  elply2  15819  plymullem1  15832  plycolemc  15842  plycjlemc  15844  dvply1  15849  pilem3  15867  relogeftb  15949  logbgcd1irr  16052  birthdaylem3  16072  mpodvdsmulf1o  16087  mersenne  16094  lgslem4  16105  lgsval  16106  lgsfvalg  16107  lgsval2lem  16112  lgsmod  16128  lgsdir2lem4  16133  lgsdinn0  16150  lgsquad2lem2  16184  lgsquad3  16186  2lgslem1c  16192  2sqlem6  16222  2sqlem7  16223  isupgren  16319  wrdupgren  16320  isumgren  16329  wrdumgren  16330  isuspgren  16381  isusgren  16382  clwwlkext2edg  16646  clwwlknonex2  16663  depindlem3  16732  pw1map  17008  nnsf  17022  peano4nninf  17023  nninfalllem1  17025  nninfsellemqall  17032  nninfsellemeqinf  17033  nninffeq  17037  exmidsbthrlem  17041  isomninnlem  17053  iswomninnlem  17073  iswomni0  17075  ismkvnnlem  17076