Theorem 3adantr3 1172

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

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

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 1088

This theorem is referenced by:  3adant3r3  1185  3ad2antr1  1189  3ad2antr2  1190  sotr2  5566  dfwe2  7719  smogt  8299  infsupprpr  9409  wlogle  11670  fzadd2  13475  swrdspsleq  14589  tanadd  16092  prdssgrpd  18658  prdsmndd  18695  mhmmnd  18994  imasrng  20112  imasring  20266  prdslmodd  20920  sraassab  21823  mpllsslem  21955  scmatlss  22469  mdetunilem3  22558  ptclsg  23559  tmdgsum2  24040  isxmet2d  24271  xmetres2  24305  prdsxmetlem  24312  comet  24457  iimulcl  24889  icoopnst  24892  iocopnst  24893  icccvx  24904  dvfsumrlim  25994  dvfsumrlim2  25995  colhp  28842  eengtrkg  29059  wwlksnredwwlkn  29968  dmdsl3  32390  eqgvscpbl  33431  resconn  35440  poimirlem28  37849  poimirlem32  37853  broucube  37855  ftc1anclem7  37900  ftc1anc  37902  isdrngo2  38159  iscringd  38199  unichnidl  38232  lplnle  39800  2llnjN  39827  2lplnj  39880  osumcllem11N  40226  cdleme1  40487  erngplus2  41064  erngplus2-rN  41072  erngdvlem3  41250  erngdvlem3-rN  41258  dvaplusgv  41270  dvalveclem  41285  dvhvaddass  41357  dvhlveclem  41368  dihmeetlem12N  41578  issmflem  46971  fmtnoprmfac1  47811  lincresunit3lem2  48726  lincresunit3  48727