Theorem 3adantr3 1173

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

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

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 1089

This theorem is referenced by:  3adant3r3  1186  3ad2antr1  1190  3ad2antr2  1191  sotr2  5566  dfwe2  7721  smogt  8300  infsupprpr  9412  wlogle  11674  fzadd2  13504  swrdspsleq  14619  tanadd  16125  prdssgrpd  18692  prdsmndd  18729  mhmmnd  19031  imasrng  20149  imasring  20301  prdslmodd  20955  sraassab  21858  mpllsslem  21988  scmatlss  22500  mdetunilem3  22589  ptclsg  23590  tmdgsum2  24071  isxmet2d  24302  xmetres2  24336  prdsxmetlem  24343  comet  24488  iimulcl  24914  icoopnst  24916  iocopnst  24917  icccvx  24927  dvfsumrlim  26008  dvfsumrlim2  26009  colhp  28852  eengtrkg  29069  wwlksnredwwlkn  29978  dmdsl3  32401  eqgvscpbl  33425  resconn  35444  poimirlem28  37983  poimirlem32  37987  broucube  37989  ftc1anclem7  38034  ftc1anc  38036  isdrngo2  38293  iscringd  38333  unichnidl  38366  lplnle  40000  2llnjN  40027  2lplnj  40080  osumcllem11N  40426  cdleme1  40687  erngplus2  41264  erngplus2-rN  41272  erngdvlem3  41450  erngdvlem3-rN  41458  dvaplusgv  41470  dvalveclem  41485  dvhvaddass  41557  dvhlveclem  41568  dihmeetlem12N  41778  issmflem  47173  fmtnoprmfac1  48040  lincresunit3lem2  48968  lincresunit3  48969