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  863  pm5.11dc  910  ax16i  1868  mor  2078  ceqsalg  2777  cgsexg  2784  cgsex2g  2785  cgsex4g  2786  spc2egv  2839  spc2gv  2840  spc3egv  2841  spc3gv  2842  disjne  3488  uneqdifeqim  3520  eqifdc  3581  triun  4126  sucssel  4436  ordsucg  4513  regexmidlem1  4544  relresfld  5170  relcoi1  5172  focdmex  6129  f1dmex  6130  dom2d  6786  findcard  6901  nneo  9369  zeo2  9372  uznfz  10116  difelfzle  10147  ssfzo12  10237  facndiv  10732  fisumcom2  11459  fprodssdc  11611  fprodcom2fi  11647  ndvdssub  11948  bezoutlembi  12019  eucalglt  12070  prmind2  12133  coprm  12157  prmdiveq  12249  mhmlin  12879  issubg2m  13080  nsgbi  13095  issubrng2  13425  issubrg2  13456  lmodlema  13476  rmodislmodlem  13534  rmodislmod  13535  lspsnel6  13592  inopn  13774  basis1  13818  tgss  13834  tgcl  13835  xmeteq0  14130  blssexps  14200  blssex  14201  mopni3  14255  neibl  14262  metss  14265  metcnp3  14282  logbgcd1irr  14656  2lgsoddprmlem3  14730  bj-indsuc  14951  bj-nntrans  14974