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  5564  dfwe2  7719  smogt  8298  infsupprpr  9410  wlogle  11672  fzadd2  13502  swrdspsleq  14617  tanadd  16123  prdssgrpd  18690  prdsmndd  18727  mhmmnd  19029  imasrng  20147  imasring  20299  prdslmodd  20953  sraassab  21856  mpllsslem  21987  scmatlss  22499  mdetunilem3  22588  ptclsg  23589  tmdgsum2  24070  isxmet2d  24301  xmetres2  24335  prdsxmetlem  24342  comet  24487  iimulcl  24913  icoopnst  24915  iocopnst  24916  icccvx  24926  dvfsumrlim  26010  dvfsumrlim2  26011  colhp  28857  eengtrkg  29074  wwlksnredwwlkn  29983  dmdsl3  32406  eqgvscpbl  33430  resconn  35449  poimirlem28  37980  poimirlem32  37984  broucube  37986  ftc1anclem7  38031  ftc1anc  38033  isdrngo2  38290  iscringd  38330  unichnidl  38363  lplnle  39997  2llnjN  40024  2lplnj  40077  osumcllem11N  40423  cdleme1  40684  erngplus2  41261  erngplus2-rN  41269  erngdvlem3  41447  erngdvlem3-rN  41455  dvaplusgv  41467  dvalveclem  41482  dvhvaddass  41554  dvhlveclem  41565  dihmeetlem12N  41775  issmflem  47170  fmtnoprmfac1  48025  lincresunit3lem2  48953  lincresunit3  48954