Theorem 3adantr3 1184

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  3adant3r3  1197  3ad2antr1  1201  3ad2antr2  1202  sotr2  5585  dfwe2  7751  smogt  8331  infsupprpr  9445  wlogle  11713  fzadd2  13557  swrdspsleq  14672  tanadd  16189  prdssgrpd  18757  prdsmndd  18794  mhmmnd  19096  imasrng  20213  imasring  20365  prdslmodd  21023  sraassab  21907  mpllsslem  22038  scmatlss  22572  mdetunilem3  22661  ptclsg  23662  tmdgsum2  24143  isxmet2d  24374  xmetres2  24408  prdsxmetlem  24415  comet  24560  iimulcl  24986  icoopnst  24988  iocopnst  24989  icccvx  24999  dvfsumrlim  26080  dvfsumrlim2  26081  colhp  28926  eengtrkg  29143  wwlksnredwwlkn  30051  dmdsl3  32474  eqgvscpbl  33496  resconn  35556  poimirlem28  38107  poimirlem32  38111  broucube  38113  ftc1anclem7  38158  ftc1anc  38160  isdrngo2  38417  iscringd  38457  unichnidl  38490  lplnle  40124  2llnjN  40151  2lplnj  40204  osumcllem11N  40550  cdleme1  40811  erngplus2  41388  erngplus2-rN  41396  erngdvlem3  41574  erngdvlem3-rN  41582  dvaplusgv  41594  dvalveclem  41609  dvhvaddass  41681  dvhlveclem  41692  dihmeetlem12N  41902  issmflem  47261  fmtnoprmfac1  48134  lincresunit3lem2  49062  lincresunit3  49063