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  5569  fprlem1  8322  unblem1  9288  frrlem15  9765  prodgt02  12169  lo1mul  15801  infpnlem1  17094  matunitlindflem1  23000  ghmcnp  24440  ulmcaulem  26727  ulmcau  26728  shintcli  31937  ballotlemfc0  35172  ballotlemfcc  35173  kardfi  35895  btwnxfr  36914  endofsegid  36943  bj-bary1lem1  38326  ltcvrntr  40575  poml4N  41104