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  5608  dfwe2  7782  smogt  8363  infsupprpr  9476  wlogle  11765  fzadd2  13606  swrdspsleq  14727  tanadd  16248  prdssgrpd  18820  prdsmndd  18859  mhmmnd  19161  imasrng  20286  imasring  20445  prdslmodd  21127  sraassab  22055  mpllsslem  22186  scmatlss  22719  mdetunilem3  22808  ptclsg  23809  tmdgsum2  24290  isxmet2d  24521  xmetres2  24555  prdsxmetlem  24562  comet  24707  iimulcl  25133  icoopnst  25135  iocopnst  25136  icccvx  25146  dvfsumrlim  26227  dvfsumrlim2  26228  colhp  29089  eengtrkg  29373  wwlksnredwwlkn  30281  dmdsl3  32704  eqgvscpbl  33701  resconn  35759  poimirlem28  38340  poimirlem32  38344  broucube  38346  ftc1anclem7  38391  ftc1anc  38393  isdrngo2  38650  iscringd  38690  unichnidl  38723  lplnle  40355  2llnjN  40382  2lplnj  40435  osumcllem11N  40781  cdleme1  41042  erngplus2  41619  erngplus2-rN  41627  erngdvlem3  41805  erngdvlem3-rN  41813  dvaplusgv  41825  dvalveclem  41840  dvhvaddass  41912  dvhlveclem  41923  dihmeetlem12N  42133  issmflem  47482  fmtnoprmfac1  48358  lincresunit3lem2  49301  lincresunit3  49302