Theorem 3adantr3 1173

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)

Hypothesis

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

Assertion

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

Proof of Theorem 3adantr3

Step	Hyp	Ref	Expression
1		3simpa 1149	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜒))
2		3adantr.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 594	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

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

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 1089

This theorem is referenced by:  3adant3r3  1186  3ad2antr1  1190  3ad2antr2  1191  sotr2  5573  dfwe2  7728  smogt  8307  infsupprpr  9419  wlogle  11683  fzadd2  13513  swrdspsleq  14628  tanadd  16134  prdssgrpd  18701  prdsmndd  18738  mhmmnd  19040  imasrng  20158  imasring  20310  prdslmodd  20964  sraassab  21848  mpllsslem  21978  scmatlss  22490  mdetunilem3  22579  ptclsg  23580  tmdgsum2  24061  isxmet2d  24292  xmetres2  24326  prdsxmetlem  24333  comet  24478  iimulcl  24904  icoopnst  24906  iocopnst  24907  icccvx  24917  dvfsumrlim  25998  dvfsumrlim2  25999  colhp  28838  eengtrkg  29055  wwlksnredwwlkn  29963  dmdsl3  32386  eqgvscpbl  33410  resconn  35428  poimirlem28  37969  poimirlem32  37973  broucube  37975  ftc1anclem7  38020  ftc1anc  38022  isdrngo2  38279  iscringd  38319  unichnidl  38352  lplnle  39986  2llnjN  40013  2lplnj  40066  osumcllem11N  40412  cdleme1  40673  erngplus2  41250  erngplus2-rN  41258  erngdvlem3  41436  erngdvlem3-rN  41444  dvaplusgv  41456  dvalveclem  41471  dvhvaddass  41543  dvhlveclem  41554  dihmeetlem12N  41764  issmflem  47155  fmtnoprmfac1  48028  lincresunit3lem2  48956  lincresunit3  48957