Theorem 3adantr3 1172

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

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

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 1088

This theorem is referenced by:  3adant3r3  1185  3ad2antr1  1189  3ad2antr2  1190  sotr2  5565  dfwe2  7714  smogt  8297  infsupprpr  9415  wlogle  11671  fzadd2  13480  swrdspsleq  14590  tanadd  16094  prdssgrpd  18625  prdsmndd  18662  mhmmnd  18961  imasrng  20080  imasring  20233  prdslmodd  20890  sraassab  21793  mpllsslem  21925  scmatlss  22428  mdetunilem3  22517  ptclsg  23518  tmdgsum2  23999  isxmet2d  24231  xmetres2  24265  prdsxmetlem  24272  comet  24417  iimulcl  24849  icoopnst  24852  iocopnst  24853  icccvx  24864  dvfsumrlim  25954  dvfsumrlim2  25955  colhp  28733  eengtrkg  28949  wwlksnredwwlkn  29858  dmdsl3  32277  eqgvscpbl  33297  resconn  35218  poimirlem28  37627  poimirlem32  37631  broucube  37633  ftc1anclem7  37678  ftc1anc  37680  isdrngo2  37937  iscringd  37977  unichnidl  38010  lplnle  39519  2llnjN  39546  2lplnj  39599  osumcllem11N  39945  cdleme1  40206  erngplus2  40783  erngplus2-rN  40791  erngdvlem3  40969  erngdvlem3-rN  40977  dvaplusgv  40989  dvalveclem  41004  dvhvaddass  41076  dvhlveclem  41087  dihmeetlem12N  41297  issmflem  46709  fmtnoprmfac1  47550  lincresunit3lem2  48466  lincresunit3  48467