Theorem 3adantr3 1222

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3ad2antr1  1226  3ad2antr2  1227  3adant3r3  1276  sotr2  5064  dfwe2  6981  smogt  7464  wlogle  10561  fzadd2  12376  tanadd  14897  prdsmndd  17323  mhmmnd  17537  imasring  18619  prdslmodd  18969  mpllsslem  19435  scmatlss  20331  mdetunilem3  20420  ptclsg  21418  tmdgsum2  21900  isxmet2d  22132  xmetres2  22166  prdsxmetlem  22173  comet  22318  iimulcl  22736  icoopnst  22738  iocopnst  22739  icccvx  22749  dvfsumrlim  23794  dvfsumrlim2  23795  colhp  25662  eengtrkg  25865  wwlksnredwwlkn  26790  dmdsl3  29174  resconn  31228  poimirlem28  33437  poimirlem32  33441  broucube  33443  ftc1anclem7  33491  ftc1anc  33493  isdrngo2  33757  iscringd  33797  unichnidl  33830  lplnle  34826  2llnjN  34853  2lplnj  34906  osumcllem11N  35252  cdleme1  35514  erngplus2  36092  erngplus2-rN  36100  erngdvlem3  36278  erngdvlem3-rN  36286  dvaplusgv  36298  dvalveclem  36314  dvhvaddass  36386  dvhlveclem  36397  dihmeetlem12N  36607  issmflem  40936  fmtnoprmfac1  41477  lincresunit3lem2  42269  lincresunit3  42270