Theorem sylan2d 605

Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.)

Hypotheses

Ref	Expression
sylan2d.1	⊢ (𝜑 → (𝜓 → 𝜒))
sylan2d.2	⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜏))

Assertion

Ref	Expression
sylan2d	⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜏))

Proof of Theorem sylan2d

Step	Hyp	Ref	Expression
1		sylan2d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylan2d.2	. . . 4 ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜏))
3	2	ancomsd 466	. . 3 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜏))
4	1, 3	syland 603	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜏))
5	4	ancomsd 466	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜏))

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  sylan2i  606  syl2and  608  swopo  5514  fprlem1  8116  wfrlem5OLD  8144  unblem1  9066  unfiOLD  9081  frrlem15  9515  prodgt02  11823  lo1mul  15337  infpnlem1  16611  ghmcnp  23266  ulmcaulem  25553  ulmcau  25554  shintcli  29691  ballotlemfc0  32459  ballotlemfcc  32460  btwnxfr  34358  endofsegid  34387  bj-bary1lem1  35482  matunitlindflem1  35773  ltcvrntr  37438  poml4N  37967