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 ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad3antlr  497  simplr  533  simplrl  541  simplrr  542  ordtri2or2exmidlem  4673  en2lp  4701  foun  5658  f1oprg  5685  fcof1o  5995  foeqcnvco  5996  f1eqcocnv  5997  caovord3  6263  f1o2ndf1  6464  suppfnss  6497  suppssdc  6500  suppssfvg  6503  smores2  6565  frecrdg  6679  nnaordex  6801  xpdom2  7129  xpen  7145  mapen  7146  xpmapenlem  7149  nndomo  7165  phpm  7167  fidifsnen  7172  isinfinf  7201  fidcen  7203  finexdc  7207  elssdc  7209  fientri3  7222  fiintim  7238  xpfi  7239  f1dmvrnfibi  7258  sbthlemi8  7281  2omap  7318  2omapfi  7320  djudom  7433  omp1eomlem  7434  difinfsn  7440  ctmlemr  7448  ctssdccl  7451  nnnninfeq  7468  enomnilem  7478  finomni  7480  ismkvnex  7495  enmkvlem  7501  nninfwlpoimlemginf  7516  exmidfodomrlemrALT  7555  exmidontriim  7581  netap  7620  exmidapne  7626  acnccim  7638  dfplpq2  7721  recclnq  7759  subhalfnqq  7781  distrnq0  7826  prarloclem3step  7863  genpml  7884  genpmu  7885  addnqprl  7896  addnqpru  7897  appdivnq  7930  mulnqprl  7935  mulnqpru  7936  mullocpr  7938  ltexprlemfl  7976  ltexprlemfu  7978  ltmprr  8009  archpr  8010  cauappcvgprlemm  8012  caucvgprlemladdrl  8045  caucvgprprlemopl  8064  caucvgprprlemopu  8066  recexgt0sr  8140  mulgt0sr  8145  elrealeu  8196  axcaucvglemcau  8265  axcaucvglemres  8266  cnegex  8504  apirr  8934  mulge0  8948  lemul12a  9193  lediv2a  9226  creur  9290  nndiv  9346  zaddcllemneg  9685  peano5uzti  9756  supinfneg  9997  infsupneg  9998  divfnzn  10023  xrltso  10200  xpncan  10275  xltadd1  10280  xleaddadd  10291  elioc2  10340  elico2  10341  elicc2  10342  exfzdc  10661  zsupcllemstep  10664  infssuzex  10668  suprzubdc  10673  exbtwnzlemex  10686  rebtwn2z  10691  modqid  10788  modqcyc  10798  mulqaddmodid  10803  modqadd2mod  10813  addmodlteq  10837  frecuzrdgg  10855  nninfinf  10882  seq3val  10899  seqvalcd  10900  seq3clss  10910  iseqf1olemqcl  10938  iseqf1olemnab  10940  seq3f1olemp  10954  seq3f1o  10956  seqf1oglem1  10958  seqfeq4g  10970  fser0const  10974  ser3ge0  10975  exp3vallem  10979  qsqeqor  11089  facndiv  11179  faclbnd  11181  bcval5  11203  hashen  11225  fihashdom  11245  hashunlem  11246  hashfacen  11286  zfz1isolemiso  11293  seq3coll  11296  ccatsymb  11372  ccatrn  11379  ccatw2s1p2  11416  swrdccatin1  11499  swrdccatin2  11503  swrdccat3b  11514  caucvgre  11749  resqrexlemlo  11781  cau3lem  11882  qdenre  11970  rexico  11989  fimaxre2  11995  2zinfmin  12011  xrmaxiflemcl  12013  xrmaxifle  12014  xrmaxiflemcom  12017  2clim  12069  cn1lem  12082  climsqz  12103  climsqz2  12104  climcau  12115  sumrbdclem  12146  summodclem2a  12150  fsum3  12156  fsumcl2lem  12167  fsumadd  12175  sumsnf  12178  fsum2dlemstep  12203  fisum0diag2  12216  fsummulc2  12217  mertenslemub  12303  mertenslemi1  12304  mertensabs  12306  ntrivcvgap  12317  prodrbdclem  12340  prodmodclem3  12344  prodmodclem2a  12345  prodmodc  12347  prod1dc  12355  prodsnf  12361  fprod2dlemstep  12391  efaddlem  12443  tanaddaplem  12507  zdvdsdc  12581  dvdseq  12617  dvdsext  12624  odd2np1  12642  sqoddm1div8z  12655  nno  12675  dfgcd3  12789  nninfctlemfo  12819  dvdslcm  12849  lcmneg  12854  lcmgcdlem  12857  ncoprmgcdne1b  12869  qredeq  12876  qredeu  12877  divgcdcoprm0  12881  exprmfct  12918  prmdvdsfz  12919  isprm5  12922  rpexp1i  12934  sqrt2irr  12942  nonsq  12987  eulerthlemrprm  13009  eulerthlema  13010  phisum  13021  modprmn0modprm0  13037  pclemdc  13069  pcz  13113  pcmpt  13124  fldivp1  13129  pcfac  13131  expnprm  13134  oddprmdvds  13135  prmpwdvds  13136  infpnlem1  13140  1arith  13148  4sqlem2  13170  4sqlemafi  13176  4sqleminfi  13178  4sqexercise2  13180  4sqlemsdc  13181  ballotfilemsv  13255  ballotfilemsima  13261  ctinfom  13321  enctlem  13325  nninfdclemlt  13344  setsfun  13389  setsfun0  13390  setscom  13394  gzsumfzval  13713  mndissubm  13784  resmhm  13796  resmhm2  13797  mhmco  13799  gzsumwsubmcl  13803  gzsumwmhm  13805  dfgrp2  13834  isgrpinv  13861  mulgval  13927  mulgnnp1  13935  mulgz  13955  grpissubg  13999  resghm  14065  qusecsub  14137  gsumf1ofi  14162  isrng  14235  lmodfopne  14665  dflidl2rng  14820  mulgrhm2  14947  znidomb  14995  znunit  14996  issubassa2  15037  psrbaglesuppg  15059  psrbagfi  15061  tgdom  15175  ssrest  15285  cnfval  15297  cnpfval  15298  cnpval  15301  iscnp3  15306  ssidcn  15313  cnpnei  15322  cnntr  15328  cncnp  15333  cnptopresti  15341  tx1cn  15372  upxp  15375  imasnopn  15402  bdmet  15605  metcnp  15615  ivthinclemlr  15740  ivthinclemur  15742  ivthinc  15746  dvrecap  15816  dvmptfsum  15828  elply2  15838  plymullem1  15851  plycolemc  15861  plycjlemc  15863  dvply1  15868  pilem3  15887  relogeftb  15969  logbgcd1irr  16075  birthdaylem3  16095  mpodvdsmulf1o  16110  mersenne  16117  lgslem4  16134  lgsval  16135  lgsfvalg  16136  lgsval2lem  16141  lgsmod  16157  lgsdir2lem4  16162  lgsdinn0  16179  lgsquad2lem2  16213  lgsquad3  16215  2lgslem1c  16221  2sqlem6  16251  2sqlem7  16252  isupgren  16348  wrdupgren  16349  isumgren  16358  wrdumgren  16359  isuspgren  16410  isusgren  16411  clwwlkext2edg  16675  clwwlknonex2  16692  depindlem3  16761  pw1map  17037  nnsf  17060  peano4nninf  17061  nninfalllem1  17063  nninfsellemqall  17070  nninfsellemeqinf  17071  nninffeq  17075  exmidsbthrlem  17079  isomninnlem  17091  iswomninnlem  17111  iswomni0  17113  ismkvnnlem  17114