Theorem syldc 48

Description: Syllogism deduction. Commuted form of syld 47. (Contributed by BJ, 25-Oct-2021.)

Hypotheses

Ref	Expression
syld.1	|- ( ph -> ( ps -> ch ) )
syld.2	|- ( ph -> ( ch -> th ) )

Assertion

Ref	Expression
syldc	|- ( ps -> ( ph -> th ) )

Proof of Theorem syldc

Step	Hyp	Ref	Expression
1		syld.1	. . 3 |- ( ph -> ( ps -> ch ) )
2		syld.2	. . 3 |- ( ph -> ( ch -> th ) )
3	1, 2	syld 47	. 2 |- ( ph -> ( ps -> th ) )
4	3	com12 32	1 |- ( ps -> ( ph -> th ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  wfrlem12  7426  smogt  7464  inf3lem3  8527  noinfep  8557  cfsmolem  9092  genpnnp  9827  ltaddpr2  9857  fzen  12358  hashge2el2dif  13262  lcmf  15346  ncoprmlnprm  15436  prmgaplem7  15761  initoeu1  16661  termoeu1  16668  dfgrp3lem  17513  cply1mul  19664  scmataddcl  20322  scmatsubcl  20323  2ndcctbss  21258  fgcfil  23069  wilthlem3  24796  cusgrsize2inds  26349  0enwwlksnge1  26749  clwlkclwwlklem2  26901  clwlksfclwwlk  26962  conngrv2edg  27055  pjjsi  28559  frrlem11  31792  sltval2  31809  nosupbnd1lem5  31858  wl-dveeq12  33311  dfac21  37636  mogoldbb  41673  nnsum3primesle9  41682  evengpop3  41686  evengpoap3  41687  ztprmneprm  42125  lindslinindsimp1  42246  lindslinindsimp2lem5  42251  flnn0div2ge  42327