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 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3adant3r3  1183  3ad2antr1  1187  3ad2antr2  1188  sotr2  5629  dfwe2  7792  smogt  8405  infsupprpr  9541  wlogle  11793  fzadd2  13595  swrdspsleq  14699  tanadd  16199  prdssgrpd  18758  prdsmndd  18795  mhmmnd  19094  imasrng  20194  imasring  20343  prdslmodd  20984  sraassab  21905  mpllsslem  22037  scmatlss  22546  mdetunilem3  22635  ptclsg  23638  tmdgsum2  24119  isxmet2d  24352  xmetres2  24386  prdsxmetlem  24393  comet  24541  iimulcl  24979  icoopnst  24982  iocopnst  24983  icccvx  24994  dvfsumrlim  26086  dvfsumrlim2  26087  colhp  28792  eengtrkg  29015  wwlksnredwwlkn  29924  dmdsl3  32343  eqgvscpbl  33357  resconn  35230  poimirlem28  37634  poimirlem32  37638  broucube  37640  ftc1anclem7  37685  ftc1anc  37687  isdrngo2  37944  iscringd  37984  unichnidl  38017  lplnle  39522  2llnjN  39549  2lplnj  39602  osumcllem11N  39948  cdleme1  40209  erngplus2  40786  erngplus2-rN  40794  erngdvlem3  40972  erngdvlem3-rN  40980  dvaplusgv  40992  dvalveclem  41007  dvhvaddass  41079  dvhlveclem  41090  dihmeetlem12N  41300  issmflem  46682  fmtnoprmfac1  47489  lincresunit3lem2  48325  lincresunit3  48326