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  869  pm5.11dc  916  ax16i  1906  mor  2122  ceqsalg  2831  cgsexg  2838  cgsex2g  2839  cgsex4g  2840  spc2egv  2896  spc2gv  2897  spc3egv  2898  spc3gv  2899  disjne  3548  uneqdifeqim  3580  eqifdc  3642  triun  4200  sucssel  4521  ordsucg  4600  regexmidlem1  4631  relresfld  5266  relcoi1  5268  focdmex  6277  f1dmex  6278  dom2d  6946  findcard  7077  nneo  9583  zeo2  9586  uznfz  10338  difelfzle  10369  ssfzo12  10470  facndiv  11002  swrdswrd  11290  pfxccatin12lem2  11316  pfxccatin12  11318  pfxccat3  11319  fisumcom2  12004  fprodssdc  12156  fprodcom2fi  12192  ndvdssub  12496  bezoutlembi  12581  eucalglt  12634  prmind2  12697  coprm  12721  prmdiveq  12813  mhmlin  13555  issubg2m  13781  nsgbi  13796  issubrng2  14230  issubrg2  14261  lmodlema  14312  rmodislmodlem  14370  rmodislmod  14371  lspsnel6  14428  inopn  14733  basis1  14777  tgss  14793  tgcl  14794  xmeteq0  15089  blssexps  15159  blssex  15160  mopni3  15214  neibl  15221  metss  15224  metcnp3  15241  logbgcd1irr  15697  gausslemma2dlem0i  15792  2lgsoddprmlem3  15846  clwwlkn1loopb  16277  clwwlknonex2lem2  16295  bj-indsuc  16549  bj-nntrans  16572