Theorem 3adantr3 1215

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 1051	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜒))
2		3adantr.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 490	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3ad2antr1  1219  3ad2antr2  1220  3adant3r3  1268  sotr2  4988  dfwe2  6873  smogt  7351  wlogle  10440  fzadd2  12247  tanadd  14736  prdsmndd  17146  mhmmnd  17360  imasring  18442  prdslmodd  18790  mpllsslem  19256  scmatlss  20150  mdetunilem3  20239  ptclsg  21228  tmdgsum2  21710  isxmet2d  21942  xmetres2  21976  prdsxmetlem  21983  comet  22128  iimulcl  22544  icoopnst  22546  iocopnst  22547  icccvx  22557  dvfsumrlim  23598  dvfsumrlim2  23599  colhp  25462  eengtrkg  25665  wwlknredwwlkn  26254  dmdsl3  28558  rescon  30482  poimirlem28  32607  poimirlem32  32611  broucube  32613  ftc1anclem7  32661  ftc1anc  32663  isdrngo2  32927  iscringd  32967  unichnidl  33000  lplnle  33844  2llnjN  33871  2lplnj  33924  osumcllem11N  34270  cdleme1  34532  erngplus2  35110  erngplus2-rN  35118  erngdvlem3  35296  erngdvlem3-rN  35304  dvaplusgv  35316  dvalveclem  35332  dvhvaddass  35404  dvhlveclem  35415  dihmeetlem12N  35625  issmflem  39613  fmtnoprmfac1  40015  wwlksnredwwlkn  41101  lincresunit3lem2  42063  lincresunit3  42064