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  870  pm5.11dc  917  ax16i  1907  mor  2123  ceqsalg  2841  cgsexg  2848  cgsex2g  2849  cgsex4g  2850  spc2egv  2906  spc2gv  2907  spc3egv  2908  spc3gv  2909  disjne  3561  uneqdifeqim  3594  eqifdc  3658  triun  4220  sucssel  4544  ordsucg  4623  regexmidlem1  4654  relresfld  5291  relcoi1  5293  focdmex  6307  f1dmex  6308  dom2d  7011  findcard  7144  nneo  9680  zeo2  9683  uznfz  10436  difelfzle  10467  ssfzo12  10568  facndiv  11100  swrdswrd  11393  pfxccatin12lem2  11419  pfxccatin12  11421  pfxccat3  11422  fisumcom2  12120  fprodssdc  12272  fprodcom2fi  12308  ndvdssub  12612  bezoutlembi  12697  eucalglt  12750  prmind2  12813  coprm  12837  prmdiveq  12929  mhmlin  13672  issubg2m  13898  nsgbi  13913  issubrng2  14347  issubrg2  14378  lmodlema  14432  rmodislmodlem  14490  rmodislmod  14491  lspsnel6  14548  inopn  14860  basis1  14904  tgss  14920  tgcl  14921  xmeteq0  15216  blssexps  15286  blssex  15287  mopni3  15341  neibl  15348  metss  15351  metcnp3  15368  logbgcd1irr  15824  gausslemma2dlem0i  15922  2lgsoddprmlem3  15976  clwwlkn1loopb  16407  clwwlknonex2lem2  16425  bj-indsuc  16690  bj-nntrans  16713