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  7064  findcard  7197  nneo  9761  zeo2  9764  uznfz  10528  difelfzle  10559  ssfzo12  10660  facndiv  11200  swrdswrd  11500  pfxccatin12lem2  11526  pfxccatin12  11528  pfxccat3  11529  fisumcom2  12231  fprodssdc  12383  fprodcom2fi  12419  ndvdssub  12723  bezoutlembi  12808  eucalglt  12861  prmind2  12924  coprm  12949  prmdiveq  13044  mhmlin  13834  issubg2m  14052  nsgbi  14067  issubrng2  14628  issubrg2  14659  lmodlema  14738  rmodislmodlem  14797  rmodislmod  14798  ellspsn6  14855  inopn  15241  basis1  15285  tgss  15301  tgcl  15302  xmeteq0  15597  blssexps  15667  blssex  15668  mopni3  15722  neibl  15729  metss  15732  metcnp3  15749  logbgcd1irr  16215  gausslemma2dlem0i  16393  2lgsoddprmlem3  16447  clwwlkn1loopb  16878  clwwlknonex2lem2  16896  bj-indsuc  17171  bj-nntrans  17194