Theorem 3adant3r3 1185

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)

Hypothesis

Ref	Expression
ad4ant3.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adant3r3	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Proof of Theorem 3adant3r3

Step	Hyp	Ref	Expression
1		ad4ant3.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1120	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1172	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  infsupprpr  9457  ressress  17217  plttr  18301  plelttr  18303  latledi  18436  latmlej11  18437  latmlej21  18439  latmlej22  18440  latjass  18442  latj12  18443  latj31  18446  latdisdlem  18455  ipopos  18495  imasmnd2  18701  imasmnd  18702  grpaddsubass  18962  grpsubsub4  18965  grpnpncan  18967  imasgrp2  18987  imasgrp  18988  frgp0  19690  cmn12  19732  abladdsub  19742  imasrng  20086  imasring  20239  dvrass  20317  isdomn4  20625  lss1  20844  islmhm2  20945  zntoslem  21466  ipdir  21548  psrgrpOLD  21866  psrlmod  21869  t1sep  23257  mettri2  24229  xmetrtri  24243  xmetrtri2  24244  pi1grplem  24949  dchrabl  27165  motgrp  28470  xmstrkgc  28813  ax5seglem4  28859  grpomuldivass  30470  ablomuldiv  30481  ablodivdiv4  30483  nvmdi  30577  dipdi  30772  dipsubdir  30777  dipsubdi  30778  cgr3tr4  36040  cgr3rflx  36042  seglemin  36101  linerflx1  36137  elicc3  36305  rngosubdi  37939  rngosubdir  37940  igenval2  38060  dmncan1  38070  latmassOLD  39222  omlfh1N  39251  omlfh3N  39252  cvrnbtwn  39264  cvrnbtwn2  39268  cvrnbtwn4  39272  hlatj12  39364  cvrntr  39419  islpln2a  39542  3atnelvolN  39580  elpadd2at2  39801  paddasslem17  39830  paddass  39832  paddssw2  39838  pmapjlln1  39849  ltrn2ateq  40174  cdlemc3  40187  cdleme1b  40220  cdleme3b  40223  cdleme3c  40224  cdleme9b  40246  erngdvlem3  40984  erngdvlem3-rN  40992  dvalveclem  41019  mendlmod  43178  lincsumscmcl  48422