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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  sylan2i  606  syl2and  608  swopo  5557  fprlem1  8279  unblem1  9239  frrlem15  9710  prodgt02  12030  lo1mul  15594  infpnlem1  16881  ghmcnp  24002  ulmcaulem  26303  ulmcau  26304  shintcli  31258  ballotlemfc0  34484  ballotlemfcc  34485  btwnxfr  36044  endofsegid  36073  bj-bary1lem1  37299  matunitlindflem1  37610  ltcvrntr  39418  poml4N  39947