Theorem sylcom 51

Description: Syllogism inference with commutation of antecedents. (The proof was shortened by O'Cat, 2-Feb-2006 and shortened further by Stefan Allan, 23-Feb-2006.)

Hypotheses

Ref	Expression
sylcom.1	⊢ (φ → (ψ → χ))
sylcom.2	⊢ (ψ → (χ → θ))

Assertion

Ref	Expression
sylcom	⊢ (φ → (ψ → θ))

Proof of Theorem sylcom

Step	Hyp	Ref	Expression
1		sylcom.1	. 2 ⊢ (φ → (ψ → χ))
2		sylcom.2	. . 3 ⊢ (ψ → (χ → θ))
3	2	a2i 9	. 2 ⊢ ((ψ → χ) → (ψ → θ))
4	1, 3	syl 10	1 ⊢ (φ → (ψ → θ))

Syntax hints:   → wi 3

This theorem is referenced by:  syl5com 52  syli 54  limuni3 3206  funopg 3652  elrnoprabg 4186  tz7.49 4260  abianfp 4263  unblem3 4688  isfinite2 4692  nsmallpq 5237  uzwo4OLD 6381  uzwo 6582  uzwoOLD 6583  chcmhi 9389  h1datomi 9780  irredlem1 10599  compsublem 11487  compfipin0 11493  cncomp 11494  gafo 11773

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

Copyright terms: Public domain