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-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  com12  30  syl5  32  pm2.6dc  864  pm5.11dc  911  ax16i  1882  mor  2097  ceqsalg  2802  cgsexg  2809  cgsex2g  2810  cgsex4g  2811  spc2egv  2865  spc2gv  2866  spc3egv  2867  spc3gv  2868  disjne  3516  uneqdifeqim  3548  eqifdc  3609  triun  4160  sucssel  4476  ordsucg  4555  regexmidlem1  4586  relresfld  5218  relcoi1  5220  focdmex  6210  f1dmex  6211  dom2d  6874  findcard  6997  nneo  9489  zeo2  9492  uznfz  10238  difelfzle  10269  ssfzo12  10366  facndiv  10897  swrdswrd  11170  fisumcom2  11799  fprodssdc  11951  fprodcom2fi  11987  ndvdssub  12291  bezoutlembi  12376  eucalglt  12429  prmind2  12492  coprm  12516  prmdiveq  12608  mhmlin  13349  issubg2m  13575  nsgbi  13590  issubrng2  14022  issubrg2  14053  lmodlema  14104  rmodislmodlem  14162  rmodislmod  14163  lspsnel6  14220  inopn  14525  basis1  14569  tgss  14585  tgcl  14586  xmeteq0  14881  blssexps  14951  blssex  14952  mopni3  15006  neibl  15013  metss  15016  metcnp3  15033  logbgcd1irr  15489  gausslemma2dlem0i  15584  2lgsoddprmlem3  15638  bj-indsuc  15978  bj-nntrans  16001