Theorem 3adant3r3 1184

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 1171	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  9545  ressress  17294  plttr  18388  plelttr  18390  latledi  18523  latmlej11  18524  latmlej21  18526  latmlej22  18527  latjass  18529  latj12  18530  latj31  18533  latdisdlem  18542  ipopos  18582  imasmnd2  18788  imasmnd  18789  grpaddsubass  19049  grpsubsub4  19052  grpnpncan  19054  imasgrp2  19074  imasgrp  19075  frgp0  19779  cmn12  19821  abladdsub  19831  imasrng  20175  imasring  20328  dvrass  20409  isdomn4  20717  lss1  20937  islmhm2  21038  zntoslem  21576  ipdir  21658  psrgrpOLD  21978  psrlmod  21981  t1sep  23379  mettri2  24352  xmetrtri  24366  xmetrtri2  24367  pi1grplem  25083  dchrabl  27299  motgrp  28552  xmstrkgc  28901  ax5seglem4  28948  grpomuldivass  30561  ablomuldiv  30572  ablodivdiv4  30574  nvmdi  30668  dipdi  30863  dipsubdir  30868  dipsubdi  30869  cgr3tr4  36054  cgr3rflx  36056  seglemin  36115  linerflx1  36151  elicc3  36319  rngosubdi  37953  rngosubdir  37954  igenval2  38074  dmncan1  38084  latmassOLD  39231  omlfh1N  39260  omlfh3N  39261  cvrnbtwn  39273  cvrnbtwn2  39277  cvrnbtwn4  39281  hlatj12  39373  cvrntr  39428  islpln2a  39551  3atnelvolN  39589  elpadd2at2  39810  paddasslem17  39839  paddass  39841  paddssw2  39847  pmapjlln1  39858  ltrn2ateq  40183  cdlemc3  40196  cdleme1b  40229  cdleme3b  40232  cdleme3c  40233  cdleme9b  40255  erngdvlem3  40993  erngdvlem3-rN  41001  dvalveclem  41028  mendlmod  43206  lincsumscmcl  48355