Theorem sylan2i 468

Description: A syllogism inference.

Hypotheses

Ref	Expression
sylan2i.1	⊢ (φ → ((ψ ⋀ χ) → θ))
sylan2i.2	⊢ (τ → χ)

Assertion

Ref	Expression
sylan2i	⊢ (φ → ((ψ ⋀ τ) → θ))

Proof of Theorem sylan2i

Step	Hyp	Ref	Expression
1		sylan2i.1	. 2 ⊢ (φ → ((ψ ⋀ χ) → θ))
2		sylan2i.2	. . 3 ⊢ (τ → χ)
3	2	a1i 8	. 2 ⊢ (φ → (τ → χ))
4	1, 3	sylan2d 461	1 ⊢ (φ → ((ψ ⋀ τ) → θ))

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  syl2ani 469  odi 4224  sdomentr 4485  sdomtr 4489  pssnn 4549  noinfep 4652  rankr1 4686  ltaddpr 5153  ltexprlem7 5161  ltaprlem 5163  prlem936b 5167  reclem3pr 5171  divdivdivt 5789  sup2 6057  lmcau 8005  spanunsn 9509  pjnormss 10103

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain