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  4244  sucssel  4571  ordsucg  4651  regexmidlem1  4682  relresfld  5320  relcoi1  5322  focdmex  6348  f1dmex  6349  dom2d  7065  findcard  7198  nneo  9760  zeo2  9763  uznfz  10527  difelfzle  10558  ssfzo12  10659  facndiv  11199  swrdswrd  11499  pfxccatin12lem2  11525  pfxccatin12  11527  pfxccat3  11528  fisumcom2  12230  fprodssdc  12382  fprodcom2fi  12418  ndvdssub  12722  bezoutlembi  12807  eucalglt  12860  prmind2  12923  coprm  12948  prmdiveq  13043  mhmlin  13833  issubg2m  14051  nsgbi  14066  issubrng2  14627  issubrg2  14658  lmodlema  14737  rmodislmodlem  14796  rmodislmod  14797  ellspsn6  14854  inopn  15262  basis1  15306  tgss  15322  tgcl  15323  xmeteq0  15618  blssexps  15688  blssex  15689  mopni3  15743  neibl  15750  metss  15753  metcnp3  15770  logbgcd1irr  16236  gausslemma2dlem0i  16414  2lgsoddprmlem3  16468  clwwlkn1loopb  16899  clwwlknonex2lem2  16917  bj-indsuc  17192  bj-nntrans  17215