Theorem 3adantr3 1190

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adant3r3  1203  3ad2antr1  1207  3ad2antr2  1208  sotr2  5601  dfwe2  7777  smogt  8360  infsupprpr  9480  wlogle  11775  fzadd2  13618  swrdspsleq  14739  tanadd  16261  prdssgrpd  18841  prdsmndd  18883  mhmmnd  19193  imasrng  20318  imasring  20477  prdslmodd  21159  sraassab  22089  mpllsslem  22220  scmatlss  22753  mdetunilem3  22842  ptclsg  23847  tmdgsum2  24328  isxmet2d  24559  xmetres2  24593  prdsxmetlem  24600  comet  24745  iimulcl  25171  icoopnst  25173  iocopnst  25174  icccvx  25184  dvfsumrlim  26265  dvfsumrlim2  26266  colhp  29135  eengtrkg  29451  wwlksnredwwlkn  30371  dmdsl3  32804  eqgvscpbl  33798  resconn  35833  poimirlem28  38405  poimirlem32  38409  broucube  38411  ftc1anclem7  38456  ftc1anc  38458  isdrngo2  38716  iscringd  38756  unichnidl  38789  lplnle  40421  2llnjN  40448  2lplnj  40501  osumcllem11N  40847  cdleme1  41108  erngplus2  41685  erngplus2-rN  41693  erngdvlem3  41871  erngdvlem3-rN  41879  dvaplusgv  41891  dvalveclem  41906  dvhvaddass  41978  dvhlveclem  41989  dihmeetlem12N  42199  issmflem  47563  fmtnoprmfac1  48476  lincresunit3lem2  49418  lincresunit3  49419