Theorem 3adantr3 1170

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

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

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

This theorem is referenced by:  3adant3r3  1183  3ad2antr1  1187  3ad2antr2  1188  sotr2  5535  dfwe2  7624  smogt  8198  infsupprpr  9263  wlogle  11508  fzadd2  13291  swrdspsleq  14378  tanadd  15876  prdsmndd  18418  mhmmnd  18697  imasring  19858  prdslmodd  20231  mpllsslem  21206  scmatlss  21674  mdetunilem3  21763  ptclsg  22766  tmdgsum2  23247  isxmet2d  23480  xmetres2  23514  prdsxmetlem  23521  comet  23669  iimulcl  24100  icoopnst  24102  iocopnst  24103  icccvx  24113  dvfsumrlim  25195  dvfsumrlim2  25196  colhp  27131  eengtrkg  27354  wwlksnredwwlkn  28260  dmdsl3  30677  eqgvscpbl  31550  resconn  33208  poimirlem28  35805  poimirlem32  35809  broucube  35811  ftc1anclem7  35856  ftc1anc  35858  isdrngo2  36116  iscringd  36156  unichnidl  36189  lplnle  37554  2llnjN  37581  2lplnj  37634  osumcllem11N  37980  cdleme1  38241  erngplus2  38818  erngplus2-rN  38826  erngdvlem3  39004  erngdvlem3-rN  39012  dvaplusgv  39024  dvalveclem  39039  dvhvaddass  39111  dvhlveclem  39122  dihmeetlem12N  39332  issmflem  44263  fmtnoprmfac1  45017  lincresunit3lem2  45821  lincresunit3  45822