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  529  simplrl  537  simplrr  538  ordtri2or2exmidlem  4624  en2lp  4652  foun  5602  f1oprg  5629  fcof1o  5930  foeqcnvco  5931  f1eqcocnv  5932  caovord3  6196  f1o2ndf1  6393  smores2  6460  frecrdg  6574  nnaordex  6696  xpdom2  7015  xpen  7031  mapen  7032  xpmapenlem  7035  nndomo  7050  phpm  7052  fidifsnen  7057  isinfinf  7086  fidcen  7088  finexdc  7092  elssdc  7094  fientri3  7107  fiintim  7123  xpfi  7124  f1dmvrnfibi  7143  sbthlemi8  7163  djudom  7292  omp1eomlem  7293  difinfsn  7299  ctmlemr  7307  ctssdccl  7310  nnnninfeq  7327  enomnilem  7337  finomni  7339  ismkvnex  7354  enmkvlem  7360  nninfwlpoimlemginf  7375  exmidfodomrlemrALT  7414  exmidontriim  7440  netap  7473  exmidapne  7479  acnccim  7491  dfplpq2  7574  recclnq  7612  subhalfnqq  7634  distrnq0  7679  prarloclem3step  7716  genpml  7737  genpmu  7738  addnqprl  7749  addnqpru  7750  appdivnq  7783  mulnqprl  7788  mulnqpru  7789  mullocpr  7791  ltexprlemfl  7829  ltexprlemfu  7831  ltmprr  7862  archpr  7863  cauappcvgprlemm  7865  caucvgprlemladdrl  7898  caucvgprprlemopl  7917  caucvgprprlemopu  7919  recexgt0sr  7993  mulgt0sr  7998  elrealeu  8049  axcaucvglemcau  8118  axcaucvglemres  8119  cnegex  8357  apirr  8785  mulge0  8799  lemul12a  9042  lediv2a  9075  creur  9139  nndiv  9184  zaddcllemneg  9518  peano5uzti  9588  supinfneg  9829  infsupneg  9830  divfnzn  9855  xrltso  10031  xpncan  10106  xltadd1  10111  xleaddadd  10122  elioc2  10171  elico2  10172  elicc2  10173  exfzdc  10487  zsupcllemstep  10490  infssuzex  10494  suprzubdc  10497  exbtwnzlemex  10510  rebtwn2z  10515  modqid  10612  modqcyc  10622  mulqaddmodid  10627  modqadd2mod  10637  addmodlteq  10661  frecuzrdgg  10679  nninfinf  10706  seq3val  10723  seqvalcd  10724  seq3clss  10734  iseqf1olemqcl  10762  iseqf1olemnab  10764  seq3f1olemp  10778  seq3f1o  10780  seqf1oglem1  10782  seqfeq4g  10794  fser0const  10798  ser3ge0  10799  exp3vallem  10803  qsqeqor  10913  facndiv  11002  faclbnd  11004  bcval5  11026  hashen  11047  fihashdom  11067  hashunlem  11068  hashfacen  11101  zfz1isolemiso  11104  seq3coll  11107  ccatsymb  11180  ccatrn  11187  ccatw2s1p2  11224  swrdccatin1  11307  swrdccatin2  11311  swrdccat3b  11322  caucvgre  11543  resqrexlemlo  11575  cau3lem  11676  qdenre  11764  rexico  11783  fimaxre2  11789  2zinfmin  11805  xrmaxiflemcl  11807  xrmaxifle  11808  xrmaxiflemcom  11811  2clim  11863  cn1lem  11876  climsqz  11897  climsqz2  11898  climcau  11909  sumrbdclem  11940  summodclem2a  11944  fsum3  11950  fsumcl2lem  11961  fsumadd  11969  sumsnf  11972  fsum2dlemstep  11997  fisum0diag2  12010  fsummulc2  12011  mertenslemub  12097  mertenslemi1  12098  mertensabs  12100  ntrivcvgap  12111  prodrbdclem  12134  prodmodclem3  12138  prodmodclem2a  12139  prodmodc  12141  prod1dc  12149  prodsnf  12155  fprod2dlemstep  12185  efaddlem  12237  tanaddaplem  12301  zdvdsdc  12375  dvdseq  12411  dvdsext  12418  odd2np1  12436  sqoddm1div8z  12449  nno  12469  dfgcd3  12583  nninfctlemfo  12613  dvdslcm  12643  lcmneg  12648  lcmgcdlem  12651  ncoprmgcdne1b  12663  qredeq  12670  qredeu  12671  divgcdcoprm0  12675  exprmfct  12712  prmdvdsfz  12713  isprm5  12716  rpexp1i  12728  sqrt2irr  12736  nonsq  12781  eulerthlemrprm  12803  eulerthlema  12804  phisum  12815  modprmn0modprm0  12831  pclemdc  12863  pcz  12907  pcmpt  12918  fldivp1  12923  pcfac  12925  expnprm  12928  oddprmdvds  12929  prmpwdvds  12930  infpnlem1  12934  1arith  12942  4sqlem2  12964  4sqlemafi  12970  4sqleminfi  12972  4sqexercise2  12974  4sqlemsdc  12975  ctinfom  13051  enctlem  13055  nninfdclemlt  13074  setsfun  13119  setsfun0  13120  setscom  13124  gsumfzval  13476  mndissubm  13560  resmhm  13572  resmhm2  13573  mhmco  13575  gsumfzz  13580  gsumwsubmcl  13581  gsumwmhm  13583  dfgrp2  13612  isgrpinv  13639  mulgval  13711  mulgnnp1  13719  mulgz  13739  grpissubg  13783  resghm  13849  qusecsub  13920  isrng  13950  lmodfopne  14343  dflidl2rng  14498  gsumfzfsumlemm  14604  mulgrhm2  14627  znidomb  14675  znunit  14676  psrbaglesuppg  14689  psrbagfi  14690  tgdom  14799  ssrest  14909  cnfval  14921  cnpfval  14922  cnpval  14925  iscnp3  14930  ssidcn  14937  cnpnei  14946  cnntr  14952  cncnp  14957  cnptopresti  14965  tx1cn  14996  upxp  14999  imasnopn  15026  bdmet  15229  metcnp  15239  ivthinclemlr  15364  ivthinclemur  15366  ivthinc  15370  dvrecap  15440  dvmptfsum  15452  elply2  15462  plymullem1  15475  plycolemc  15485  plycjlemc  15487  dvply1  15492  pilem3  15510  relogeftb  15592  logbgcd1irr  15694  mpodvdsmulf1o  15717  mersenne  15724  lgslem4  15735  lgsval  15736  lgsfvalg  15737  lgsval2lem  15742  lgsmod  15758  lgsdir2lem4  15763  lgsdinn0  15780  lgsquad2lem2  15814  lgsquad3  15816  2lgslem1c  15822  2sqlem6  15852  2sqlem7  15853  isupgren  15949  wrdupgren  15950  isumgren  15959  wrdumgren  15960  isuspgren  16011  isusgren  16012  clwwlkext2edg  16276  clwwlknonex2  16293  depindlem3  16348  2omap  16615  pw1map  16617  nnsf  16628  peano4nninf  16629  nninfalllem1  16631  nninfsellemqall  16638  nninfsellemeqinf  16639  nninffeq  16643  exmidsbthrlem  16647  isomninnlem  16655  iswomninnlem  16674  iswomni0  16676  ismkvnnlem  16677