Theorem syl11 33

Description: A syllogism inference. Commuted form of an instance of syl 17. (Contributed by BJ, 25-Oct-2021.)

Hypotheses

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

Assertion

Ref	Expression
syl11	|- ( ps -> ( th -> ch ) )

Proof of Theorem syl11

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

Syntax hints:   -> wi 4

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

This theorem is referenced by:  pm2.86i  109  2rmorex  3412  ssprsseq  4357  elpr2elpr  4398  disjxiun  4649  oprabid  6677  elovmpt2rab  6880  elovmpt2rab1  6881  mpt2xopoveqd  7347  wfr3g  7413  oewordri  7672  fsuppunbi  8296  r1sdom  8637  pr2ne  8828  kmlem4  8975  kmlem12  8983  domtriomlem  9264  zorn2lem6  9323  axdclem  9341  wunr1om  9541  tskr1om  9589  zindd  11478  hash2pwpr  13258  fi1uzind  13279  swrdccatin2  13487  swrdccatin12  13491  repsdf2  13525  2cshwcshw  13571  cshwcshid  13573  fprodmodd  14728  alzdvds  15042  pwp1fsum  15114  lcmfdvds  15355  prm23ge5  15520  cshwshashlem2  15803  0ringnnzr  19269  01eq0ring  19272  mplcoe5lem  19467  gsummoncoe1  19674  psgndiflemA  19947  gsummatr01lem3  20463  mp2pm2mplem4  20614  fiinopn  20706  cnmptcom  21481  fgcl  21682  fmfnfmlem1  21758  fmco  21765  flffbas  21799  cnpflf2  21804  metcnp3  22345  tngngp3  22460  clmvscom  22890  aalioulem2  24088  ausgrusgrb  26060  usgredg4  26109  nbgr1vtx  26254  nbgrnself2  26259  uhgr0edg0rgrb  26470  wlkres  26567  uhgrwkspth  26651  usgr2wlkspth  26655  uspgrn2crct  26700  crctcshwlkn0  26713  wwlksnredwwlkn  26790  wwlksnextsur  26795  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  frgrnbnb  27157  frgrwopreglem5  27185  frgrwopreglem5ALT  27186  extwwlkfab  27223  cvati  29225  dmdbr5ati  29281  dfon2lem3  31690  frr3g  31779  bj-0int  33055  ptrecube  33409  fzmul  33537  zerdivemp1x  33746  psshepw  38082  ndmaovdistr  41287  ssfz12  41324  fzopredsuc  41333  smonoord  41341  iccpartltu  41361  iccpartgtl  41362  pfxccatin12  41425  lighneallem3  41524  odd2prm2  41627  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  bgoldbnnsum3prm  41692  elsprel  41725  ringcbasbas  42034  ringcbasbasALTV  42058  ply1mulgsumlem2  42175  ldepsnlinclem1  42294  ldepsnlinclem2  42295  nnolog2flm1  42384  blengt1fldiv2p1  42387