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

Syntax hints:   → wi 4   ∧ wa 394   ∧ 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 395  df-3an 1087

This theorem is referenced by:  3adant3r3  1182  3ad2antr1  1186  3ad2antr2  1187  sotr2  5619  dfwe2  7763  smogt  8369  infsupprpr  9501  wlogle  11751  fzadd2  13540  swrdspsleq  14619  tanadd  16114  prdssgrpd  18658  prdsmndd  18692  mhmmnd  18983  imasrng  20071  imasring  20218  prdslmodd  20724  sraassab  21641  mpllsslem  21778  scmatlss  22247  mdetunilem3  22336  ptclsg  23339  tmdgsum2  23820  isxmet2d  24053  xmetres2  24087  prdsxmetlem  24094  comet  24242  iimulcl  24680  icoopnst  24683  iocopnst  24684  icccvx  24695  dvfsumrlim  25783  dvfsumrlim2  25784  colhp  28288  eengtrkg  28511  wwlksnredwwlkn  29416  dmdsl3  31835  eqgvscpbl  32735  resconn  34535  poimirlem28  36819  poimirlem32  36823  broucube  36825  ftc1anclem7  36870  ftc1anc  36872  isdrngo2  37129  iscringd  37169  unichnidl  37202  lplnle  38714  2llnjN  38741  2lplnj  38794  osumcllem11N  39140  cdleme1  39401  erngplus2  39978  erngplus2-rN  39986  erngdvlem3  40164  erngdvlem3-rN  40172  dvaplusgv  40184  dvalveclem  40199  dvhvaddass  40271  dvhlveclem  40282  dihmeetlem12N  40492  issmflem  45741  fmtnoprmfac1  46531  lincresunit3lem2  47248  lincresunit3  47249