Theorem 3adantr3 1188

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3adant3r3  1201  3ad2antr1  1205  3ad2antr2  1206  sotr2  5593  dfwe2  7761  smogt  8342  infsupprpr  9454  wlogle  11735  fzadd2  13575  swrdspsleq  14691  tanadd  16211  prdssgrpd  18779  prdsmndd  18816  mhmmnd  19118  imasrng  20243  imasring  20400  prdslmodd  21056  sraassab  21975  mpllsslem  22106  scmatlss  22639  mdetunilem3  22728  ptclsg  23729  tmdgsum2  24210  isxmet2d  24441  xmetres2  24475  prdsxmetlem  24482  comet  24627  iimulcl  25053  icoopnst  25055  iocopnst  25056  icccvx  25066  dvfsumrlim  26147  dvfsumrlim2  26148  colhp  28997  eengtrkg  29241  wwlksnredwwlkn  30149  dmdsl3  32572  eqgvscpbl  33580  resconn  35604  poimirlem28  38154  poimirlem32  38158  broucube  38160  ftc1anclem7  38205  ftc1anc  38207  isdrngo2  38464  iscringd  38504  unichnidl  38537  lplnle  40171  2llnjN  40198  2lplnj  40251  osumcllem11N  40597  cdleme1  40858  erngplus2  41435  erngplus2-rN  41443  erngdvlem3  41621  erngdvlem3-rN  41629  dvaplusgv  41641  dvalveclem  41656  dvhvaddass  41728  dvhlveclem  41739  dihmeetlem12N  41949  issmflem  47300  fmtnoprmfac1  48173  lincresunit3lem2  49112  lincresunit3  49113