Theorem 3adantr3 1242

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054

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 385  df-3an 1056

This theorem is referenced by:  3ad2antr1  1246  3ad2antr2  1247  3adant3r3  1297  sotr2  5093  dfwe2  7023  smogt  7509  wlogle  10599  fzadd2  12414  tanadd  14941  prdsmndd  17370  mhmmnd  17584  imasring  18665  prdslmodd  19017  mpllsslem  19483  scmatlss  20379  mdetunilem3  20468  ptclsg  21466  tmdgsum2  21947  isxmet2d  22179  xmetres2  22213  prdsxmetlem  22220  comet  22365  iimulcl  22783  icoopnst  22785  iocopnst  22786  icccvx  22796  dvfsumrlim  23839  dvfsumrlim2  23840  colhp  25707  eengtrkg  25910  wwlksnredwwlkn  26858  dmdsl3  29302  resconn  31354  poimirlem28  33567  poimirlem32  33571  broucube  33573  ftc1anclem7  33621  ftc1anc  33623  isdrngo2  33887  iscringd  33927  unichnidl  33960  lplnle  35144  2llnjN  35171  2lplnj  35224  osumcllem11N  35570  cdleme1  35832  erngplus2  36409  erngplus2-rN  36417  erngdvlem3  36595  erngdvlem3-rN  36603  dvaplusgv  36615  dvalveclem  36631  dvhvaddass  36703  dvhlveclem  36714  dihmeetlem12N  36924  issmflem  41257  fmtnoprmfac1  41802  lincresunit3lem2  42594  lincresunit3  42595