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 ⊢ (𝜑 → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com12  30  syl5  32  pm2.6dc  874  pm5.11dc  921  ax16i  1911  mor  2129  ceqsalg  2850  cgsexg  2857  cgsex2g  2858  cgsex4g  2859  spc2egv  2915  spc2gv  2916  spc3egv  2917  spc3gv  2918  disjne  3578  uneqdifeqim  3613  eqifdc  3677  triun  4242  sucssel  4569  ordsucg  4649  regexmidlem1  4680  relresfld  5317  relcoi1  5319  focdmex  6344  f1dmex  6345  dom2d  7059  findcard  7192  nneo  9754  zeo2  9757  uznfz  10521  difelfzle  10552  ssfzo12  10653  facndiv  11192  swrdswrd  11492  pfxccatin12lem2  11518  pfxccatin12  11520  pfxccat3  11521  fisumcom2  12223  fprodssdc  12375  fprodcom2fi  12411  ndvdssub  12715  bezoutlembi  12800  eucalglt  12853  prmind2  12916  coprm  12941  prmdiveq  13036  mhmlin  13825  issubg2m  14043  nsgbi  14058  issubrng2  14569  issubrg2  14600  lmodlema  14679  rmodislmodlem  14738  rmodislmod  14739  ellspsn6  14796  inopn  15156  basis1  15200  tgss  15216  tgcl  15217  xmeteq0  15512  blssexps  15582  blssex  15583  mopni3  15637  neibl  15644  metss  15647  metcnp3  15664  logbgcd1irr  16125  gausslemma2dlem0i  16298  2lgsoddprmlem3  16352  clwwlkn1loopb  16783  clwwlknonex2lem2  16801  bj-indsuc  17076  bj-nntrans  17099