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  4558  en2lp  4586  foun  5519  f1oprg  5544  fcof1o  5832  foeqcnvco  5833  f1eqcocnv  5834  caovord3  6092  f1o2ndf1  6281  smores2  6347  frecrdg  6461  nnaordex  6581  xpdom2  6885  xpen  6901  mapen  6902  xpmapenlem  6905  nndomo  6920  phpm  6921  fidifsnen  6926  isinfinf  6953  finexdc  6958  fientri3  6971  fiintim  6985  xpfi  6986  f1dmvrnfibi  7003  sbthlemi8  7023  djudom  7152  omp1eomlem  7153  difinfsn  7159  ctmlemr  7167  ctssdccl  7170  nnnninfeq  7187  enomnilem  7197  finomni  7199  ismkvnex  7214  enmkvlem  7220  nninfwlpoimlemginf  7235  exmidfodomrlemrALT  7263  exmidontriim  7285  netap  7314  exmidapne  7320  dfplpq2  7414  recclnq  7452  subhalfnqq  7474  distrnq0  7519  prarloclem3step  7556  genpml  7577  genpmu  7578  addnqprl  7589  addnqpru  7590  appdivnq  7623  mulnqprl  7628  mulnqpru  7629  mullocpr  7631  ltexprlemfl  7669  ltexprlemfu  7671  ltmprr  7702  archpr  7703  cauappcvgprlemm  7705  caucvgprlemladdrl  7738  caucvgprprlemopl  7757  caucvgprprlemopu  7759  recexgt0sr  7833  mulgt0sr  7838  elrealeu  7889  axcaucvglemcau  7958  axcaucvglemres  7959  cnegex  8197  apirr  8624  mulge0  8638  lemul12a  8881  lediv2a  8914  creur  8978  nndiv  9023  zaddcllemneg  9356  peano5uzti  9425  supinfneg  9660  infsupneg  9661  divfnzn  9686  xrltso  9862  xpncan  9937  xltadd1  9942  xleaddadd  9953  elioc2  10002  elico2  10003  elicc2  10004  exfzdc  10307  exbtwnzlemex  10318  rebtwn2z  10323  modqid  10420  modqcyc  10430  mulqaddmodid  10435  modqadd2mod  10445  addmodlteq  10469  frecuzrdgg  10487  nninfinf  10514  seq3val  10531  seqvalcd  10532  seq3clss  10542  iseqf1olemqcl  10570  iseqf1olemnab  10572  seq3f1olemp  10586  seq3f1o  10588  seqf1oglem1  10590  seqfeq4g  10602  fser0const  10606  ser3ge0  10607  exp3vallem  10611  qsqeqor  10721  facndiv  10810  faclbnd  10812  bcval5  10834  hashen  10855  fihashdom  10874  hashunlem  10875  hashfacen  10907  zfz1isolemiso  10910  seq3coll  10913  caucvgre  11125  resqrexlemlo  11157  cau3lem  11258  qdenre  11346  rexico  11365  fimaxre2  11370  2zinfmin  11386  xrmaxiflemcl  11388  xrmaxifle  11389  xrmaxiflemcom  11392  2clim  11444  cn1lem  11457  climsqz  11478  climsqz2  11479  climcau  11490  sumrbdclem  11520  summodclem2a  11524  fsum3  11530  fsumcl2lem  11541  fsumadd  11549  sumsnf  11552  fsum2dlemstep  11577  fisum0diag2  11590  fsummulc2  11591  mertenslemub  11677  mertenslemi1  11678  mertensabs  11680  ntrivcvgap  11691  prodrbdclem  11714  prodmodclem3  11718  prodmodclem2a  11719  prodmodc  11721  prod1dc  11729  prodsnf  11735  fprod2dlemstep  11765  efaddlem  11817  tanaddaplem  11881  zdvdsdc  11955  dvdseq  11990  dvdsext  11997  odd2np1  12014  sqoddm1div8z  12027  nno  12047  zsupcllemstep  12082  infssuzex  12086  suprzubdc  12089  dfgcd3  12147  nninfctlemfo  12177  dvdslcm  12207  lcmneg  12212  lcmgcdlem  12215  ncoprmgcdne1b  12227  qredeq  12234  qredeu  12235  divgcdcoprm0  12239  exprmfct  12276  prmdvdsfz  12277  isprm5  12280  rpexp1i  12292  sqrt2irr  12300  nonsq  12345  eulerthlemrprm  12367  eulerthlema  12368  phisum  12378  modprmn0modprm0  12394  pclemdc  12426  pcz  12470  pcmpt  12481  fldivp1  12486  pcfac  12488  expnprm  12491  oddprmdvds  12492  prmpwdvds  12493  infpnlem1  12497  1arith  12505  4sqlem2  12527  4sqlemafi  12533  4sqleminfi  12535  4sqexercise2  12537  4sqlemsdc  12538  ctinfom  12585  enctlem  12589  nninfdclemlt  12608  setsfun  12653  setsfun0  12654  setscom  12658  gsumfzval  12974  mndissubm  13047  resmhm  13059  resmhm2  13060  mhmco  13062  gsumfzz  13067  gsumwsubmcl  13068  gsumwmhm  13070  dfgrp2  13099  isgrpinv  13126  mulgval  13192  mulgnnp1  13200  mulgz  13220  grpissubg  13264  resghm  13330  qusecsub  13401  isrng  13430  lmodfopne  13822  dflidl2rng  13977  gsumfzfsumlemm  14075  mulgrhm2  14098  znidomb  14146  znunit  14147  psrbaglesuppg  14158  tgdom  14240  ssrest  14350  cnfval  14362  cnpfval  14363  cnpval  14366  iscnp3  14371  ssidcn  14378  cnpnei  14387  cnntr  14393  cncnp  14398  cnptopresti  14406  tx1cn  14437  upxp  14440  imasnopn  14467  bdmet  14670  metcnp  14680  ivthinclemlr  14791  ivthinclemur  14793  ivthinc  14797  dvrecap  14862  elply2  14881  plymullem1  14894  pilem3  14918  relogeftb  15000  logbgcd1irr  15099  lgslem4  15119  lgsval  15120  lgsfvalg  15121  lgsval2lem  15126  lgsmod  15142  lgsdir2lem4  15147  lgsdinn0  15164  2sqlem6  15207  2sqlem7  15208  nnsf  15495  peano4nninf  15496  nninfalllem1  15498  nninfsellemqall  15505  nninfsellemeqinf  15506  nninffeq  15510  exmidsbthrlem  15512  isomninnlem  15520  iswomninnlem  15539  iswomni0  15541  ismkvnnlem  15542