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  5585  fprlem1  8306  unblem1  9262  frrlem15  9739  prodgt02  12081  lo1mul  15705  infpnlem1  16995  ghmcnp  24309  ulmcaulem  26594  ulmcau  26595  shintcli  31718  ballotlemfc0  34915  ballotlemfcc  34916  kardfi  35607  btwnxfr  36569  endofsegid  36598  bj-bary1lem1  37996  matunitlindflem1  38308  ltcvrntr  40239  poml4N  40768