Theorem syl5com 29

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 28	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  30  syl5  32  pm2.6dc  770  pm5.11dc  826  ax16i  1754  mor  1958  ceqsalg  2599  cgsexg  2606  cgsex2g  2607  cgsex4g  2608  spc2egv  2659  spc2gv  2660  spc3egv  2661  spc3gv  2662  disjne  3300  uneqdifeqim  3335  triun  3894  sucssel  4188  ordsucg  4255  regexmidlem1  4285  relresfld  4874  relcoi1  4876  fornex  5769  f1dmex  5770  rdgon  6003  dom2d  6283  findcard  6375  nneo  8399  zeo2  8402  uznfz  9066  difelfzle  9093  ssfzo12  9181  facndiv  9600  bj-indsuc  10411  bj-nntrans  10435