Theorem 3adantr3 1178

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3adant3r3  1191  3ad2antr1  1195  3ad2antr2  1196  sotr2  5567  dfwe2  7724  smogt  8304  infsupprpr  9416  wlogle  11681  fzadd2  13511  swrdspsleq  14626  tanadd  16132  prdssgrpd  18699  prdsmndd  18736  mhmmnd  19038  imasrng  20156  imasring  20308  prdslmodd  20966  sraassab  21850  mpllsslem  21981  scmatlss  22515  mdetunilem3  22604  ptclsg  23605  tmdgsum2  24086  isxmet2d  24317  xmetres2  24351  prdsxmetlem  24358  comet  24503  iimulcl  24929  icoopnst  24931  iocopnst  24932  icccvx  24942  dvfsumrlim  26023  dvfsumrlim2  26024  colhp  28863  eengtrkg  29080  wwlksnredwwlkn  29988  dmdsl3  32411  eqgvscpbl  33440  resconn  35481  poimirlem28  38022  poimirlem32  38026  broucube  38028  ftc1anclem7  38073  ftc1anc  38075  isdrngo2  38332  iscringd  38372  unichnidl  38405  lplnle  40039  2llnjN  40066  2lplnj  40119  osumcllem11N  40465  cdleme1  40726  erngplus2  41303  erngplus2-rN  41311  erngdvlem3  41489  erngdvlem3-rN  41497  dvaplusgv  41509  dvalveclem  41524  dvhvaddass  41596  dvhlveclem  41607  dihmeetlem12N  41817  issmflem  47177  fmtnoprmfac1  48050  lincresunit3lem2  48978  lincresunit3  48979