Theorem 3adantr3 1171

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 592	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

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

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 1089

This theorem is referenced by:  3adant3r3  1184  3ad2antr1  1188  3ad2antr2  1189  sotr2  5641  dfwe2  7809  smogt  8423  infsupprpr  9573  wlogle  11823  fzadd2  13619  swrdspsleq  14713  tanadd  16215  prdssgrpd  18771  prdsmndd  18805  mhmmnd  19104  imasrng  20204  imasring  20353  prdslmodd  20990  sraassab  21911  mpllsslem  22043  scmatlss  22552  mdetunilem3  22641  ptclsg  23644  tmdgsum2  24125  isxmet2d  24358  xmetres2  24392  prdsxmetlem  24399  comet  24547  iimulcl  24985  icoopnst  24988  iocopnst  24989  icccvx  25000  dvfsumrlim  26092  dvfsumrlim2  26093  colhp  28796  eengtrkg  29019  wwlksnredwwlkn  29928  dmdsl3  32347  eqgvscpbl  33343  resconn  35214  poimirlem28  37608  poimirlem32  37612  broucube  37614  ftc1anclem7  37659  ftc1anc  37661  isdrngo2  37918  iscringd  37958  unichnidl  37991  lplnle  39497  2llnjN  39524  2lplnj  39577  osumcllem11N  39923  cdleme1  40184  erngplus2  40761  erngplus2-rN  40769  erngdvlem3  40947  erngdvlem3-rN  40955  dvaplusgv  40967  dvalveclem  40982  dvhvaddass  41054  dvhlveclem  41065  dihmeetlem12N  41275  issmflem  46648  fmtnoprmfac1  47439  lincresunit3lem2  48209  lincresunit3  48210