Theorem 3adantr3 1169

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  3adant3r3  1182  3ad2antr1  1186  3ad2antr2  1187  sotr2  5526  dfwe2  7602  smogt  8169  infsupprpr  9193  wlogle  11438  fzadd2  13220  swrdspsleq  14306  tanadd  15804  prdsmndd  18333  mhmmnd  18612  imasring  19773  prdslmodd  20146  mpllsslem  21116  scmatlss  21582  mdetunilem3  21671  ptclsg  22674  tmdgsum2  23155  isxmet2d  23388  xmetres2  23422  prdsxmetlem  23429  comet  23575  iimulcl  24006  icoopnst  24008  iocopnst  24009  icccvx  24019  dvfsumrlim  25100  dvfsumrlim2  25101  colhp  27035  eengtrkg  27257  wwlksnredwwlkn  28161  dmdsl3  30578  eqgvscpbl  31452  resconn  33108  poimirlem28  35732  poimirlem32  35736  broucube  35738  ftc1anclem7  35783  ftc1anc  35785  isdrngo2  36043  iscringd  36083  unichnidl  36116  lplnle  37481  2llnjN  37508  2lplnj  37561  osumcllem11N  37907  cdleme1  38168  erngplus2  38745  erngplus2-rN  38753  erngdvlem3  38931  erngdvlem3-rN  38939  dvaplusgv  38951  dvalveclem  38966  dvhvaddass  39038  dvhlveclem  39049  dihmeetlem12N  39259  issmflem  44150  fmtnoprmfac1  44905  lincresunit3lem2  45709  lincresunit3  45710