Theorem sylan2d 617

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 471	. . 3 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜏))
4	1, 3	syland 615	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜏))
5	4	ancomsd 471	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜏))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylan2i  618  syl2and  620  swopo  5578  fprlem1  8303  unblem1  9266  frrlem15  9743  prodgt02  12091  lo1mul  15719  infpnlem1  17008  matunitlindflem1  22907  ghmcnp  24347  ulmcaulem  26637  ulmcau  26638  shintcli  31818  ballotlemfc0  35012  ballotlemfcc  35013  kardfi  35704  btwnxfr  36644  endofsegid  36673  bj-bary1lem1  38071  ltcvrntr  40305  poml4N  40834