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  5598  dfwe2  7815  smogt  8406  infsupprpr  9528  wlogle  11879  fzadd2  13723  swrdspsleq  14846  tanadd  16367  prdssgrpd  18954  prdsmndd  18996  mhmmnd  19306  imasrng  20432  imasring  20593  prdslmodd  21277  sraassab  22209  mpllsslem  22340  scmatlss  22873  mdetunilem3  22962  ptclsg  23967  tmdgsum2  24448  isxmet2d  24679  xmetres2  24713  prdsxmetlem  24720  comet  24865  iimulcl  25291  icoopnst  25293  iocopnst  25294  icccvx  25304  dvfsumrlim  26384  dvfsumrlim2  26385  colhp  29281  eengtrkg  29597  wwlksnredwwlkn  30517  dmdsl3  32950  eqgvscpbl  33995  resconn  36191  poimirlem28  38771  poimirlem32  38775  broucube  38777  ftc1anclem7  38822  ftc1anc  38824  isdrngo2  39095  iscringd  39135  unichnidl  39168  lplnle  40800  2llnjN  40827  2lplnj  40880  osumcllem11N  41226  cdleme1  41487  erngplus2  42064  erngplus2-rN  42072  erngdvlem3  42250  erngdvlem3-rN  42258  dvaplusgv  42270  dvalveclem  42285  dvhvaddass  42357  dvhlveclem  42368  dihmeetlem12N  42578  issmflem  47952  fmtnoprmfac1  48865  lincresunit3lem2  49807  lincresunit3  49808