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  5558  dfwe2  7707  smogt  8287  infsupprpr  9390  wlogle  11650  fzadd2  13459  swrdspsleq  14573  tanadd  16076  prdssgrpd  18641  prdsmndd  18678  mhmmnd  18977  imasrng  20096  imasring  20249  prdslmodd  20903  sraassab  21806  mpllsslem  21938  scmatlss  22441  mdetunilem3  22530  ptclsg  23531  tmdgsum2  24012  isxmet2d  24243  xmetres2  24277  prdsxmetlem  24284  comet  24429  iimulcl  24861  icoopnst  24864  iocopnst  24865  icccvx  24876  dvfsumrlim  25966  dvfsumrlim2  25967  colhp  28749  eengtrkg  28965  wwlksnredwwlkn  29874  dmdsl3  32293  eqgvscpbl  33313  resconn  35288  poimirlem28  37694  poimirlem32  37698  broucube  37700  ftc1anclem7  37745  ftc1anc  37747  isdrngo2  38004  iscringd  38044  unichnidl  38077  lplnle  39585  2llnjN  39612  2lplnj  39665  osumcllem11N  40011  cdleme1  40272  erngplus2  40849  erngplus2-rN  40857  erngdvlem3  41035  erngdvlem3-rN  41043  dvaplusgv  41055  dvalveclem  41070  dvhvaddass  41142  dvhlveclem  41153  dihmeetlem12N  41363  issmflem  46771  fmtnoprmfac1  47602  lincresunit3lem2  48518  lincresunit3  48519