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  9751  zeo2  9754  uznfz  10512  difelfzle  10543  ssfzo12  10644  facndiv  11179  swrdswrd  11479  pfxccatin12lem2  11505  pfxccatin12  11507  pfxccat3  11508  fisumcom2  12207  fprodssdc  12359  fprodcom2fi  12395  ndvdssub  12699  bezoutlembi  12784  eucalglt  12837  prmind2  12900  coprm  12924  prmdiveq  13016  mhmlin  13776  issubg2m  13994  nsgbi  14009  issubrng2  14520  issubrg2  14551  lmodlema  14630  rmodislmodlem  14689  rmodislmod  14690  ellspsn6  14747  inopn  15106  basis1  15150  tgss  15166  tgcl  15167  xmeteq0  15462  blssexps  15532  blssex  15533  mopni3  15587  neibl  15594  metss  15597  metcnp3  15614  logbgcd1irr  16075  gausslemma2dlem0i  16188  2lgsoddprmlem3  16242  clwwlkn1loopb  16673  clwwlknonex2lem2  16691  bj-indsuc  16966  bj-nntrans  16989