Theorem 3adantr3 1168

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  3adant3r3  1181  3ad2antr1  1185  3ad2antr2  1186  sotr2  5626  dfwe2  7782  smogt  8394  infsupprpr  9535  wlogle  11785  fzadd2  13576  swrdspsleq  14655  tanadd  16151  prdssgrpd  18700  prdsmndd  18734  mhmmnd  19027  imasrng  20124  imasring  20273  prdslmodd  20860  sraassab  21808  mpllsslem  21949  scmatlss  22447  mdetunilem3  22536  ptclsg  23539  tmdgsum2  24020  isxmet2d  24253  xmetres2  24287  prdsxmetlem  24294  comet  24442  iimulcl  24880  icoopnst  24883  iocopnst  24884  icccvx  24895  dvfsumrlim  25986  dvfsumrlim2  25987  colhp  28594  eengtrkg  28817  wwlksnredwwlkn  29726  dmdsl3  32145  eqgvscpbl  33086  resconn  34889  poimirlem28  37154  poimirlem32  37158  broucube  37160  ftc1anclem7  37205  ftc1anc  37207  isdrngo2  37464  iscringd  37504  unichnidl  37537  lplnle  39045  2llnjN  39072  2lplnj  39125  osumcllem11N  39471  cdleme1  39732  erngplus2  40309  erngplus2-rN  40317  erngdvlem3  40495  erngdvlem3-rN  40503  dvaplusgv  40515  dvalveclem  40530  dvhvaddass  40602  dvhlveclem  40613  dihmeetlem12N  40823  issmflem  46144  fmtnoprmfac1  46934  lincresunit3lem2  47626  lincresunit3  47627