Theorem syl5com 26

Description: Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005.)

Hypotheses

Ref	Expression
syl5com.1	⊢ (𝜑 → 𝜓)
syl5com.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
syl5com	⊢ (𝜑 → (𝜒 → 𝜃))

Proof of Theorem syl5com

Step	Hyp	Ref	Expression
1		syl5com.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1d 22	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
3		syl5com.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	sylcom 25	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4

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

This theorem is referenced by:  com12  27  syl5  28  pm2.6dc  759  pm5.11dc  815  ax16i  1738  mor  1942  ceqsalg  2582  cgsexg  2589  cgsex2g  2590  cgsex4g  2591  spc2egv  2642  spc2gv  2643  spc3egv  2644  spc3gv  2645  disjne  3273  uneqdifeqim  3308  triun  3867  sucssel  4161  ordsucg  4228  regexmidlem1  4258  relresfld  4847  relcoi1  4849  fornex  5742  f1dmex  5743  rdgon  5973  dom2d  6253  findcard  6345  nneo  8341  zeo2  8344  uznfz  8965  difelfzle  8992  ssfzo12  9080  bj-indsuc  10052  bj-nntrans  10076