Theorem 3adantr3 1157

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

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

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  3adant3r3  1176  3ad2antr1  1180  3ad2antr2  1181  sotr2  5168  dfwe2  7098  smogt  7584  wlogle  10674  fzadd2  12490  tanadd  15017  prdsmndd  17445  mhmmnd  17659  imasring  18740  prdslmodd  19092  mpllsslem  19558  scmatlss  20454  mdetunilem3  20543  ptclsg  21541  tmdgsum2  22022  isxmet2d  22254  xmetres2  22288  prdsxmetlem  22295  comet  22440  iimulcl  22858  icoopnst  22860  iocopnst  22861  icccvx  22871  dvfsumrlim  23914  dvfsumrlim2  23915  colhp  25782  eengtrkg  25985  wwlksnredwwlkn  26934  dmdsl3  29404  resconn  31456  poimirlem28  33669  poimirlem32  33673  broucube  33675  ftc1anclem7  33723  ftc1anc  33725  isdrngo2  33989  iscringd  34029  unichnidl  34062  lplnle  35246  2llnjN  35273  2lplnj  35326  osumcllem11N  35672  cdleme1  35934  erngplus2  36511  erngplus2-rN  36519  erngdvlem3  36697  erngdvlem3-rN  36705  dvaplusgv  36717  dvalveclem  36733  dvhvaddass  36805  dvhlveclem  36816  dihmeetlem12N  37026  issmflem  41359  fmtnoprmfac1  41904  lincresunit3lem2  42696  lincresunit3  42697