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	⊢ (𝜑 → (𝜓 → 𝜒))
syl11.2	⊢ (𝜃 → 𝜑)

Assertion

Ref	Expression
syl11	⊢ (𝜓 → (𝜃 → 𝜒))

Proof of Theorem syl11

Step	Hyp	Ref	Expression
1		syl11.2	. . 3 ⊢ (𝜃 → 𝜑)
2		syl11.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl 17	. 2 ⊢ (𝜃 → (𝜓 → 𝜒))
4	3	com12 32	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:  2rmorex  3745  ssprsseq  4758  elpr2elpr  4799  disjxiun  5063  oprabidw  7187  oprabid  7188  elovmporab  7391  elovmporab1w  7392  elovmporab1  7393  mpoxopoveqd  7887  wfr3g  7953  oewordri  8218  fsuppunbi  8854  r1sdom  9203  updjud  9363  pr2ne  9431  kmlem4  9579  kmlem12  9587  domtriomlem  9864  zorn2lem6  9923  axdclem  9941  wunr1om  10141  tskr1om  10189  zindd  12084  hash2pwpr  13835  fi1uzind  13856  swrdnd0  14019  pfxccatin12  14095  repsdf2  14140  2cshwcshw  14187  cshwcshid  14189  fprodmodd  15351  alzdvds  15670  pwp1fsum  15742  lcmfdvds  15986  prm23ge5  16152  cshwshashlem2  16430  0ringnnzr  20042  01eq0ring  20045  mplcoe5lem  20248  gsummoncoe1  20472  psgndiflemA  20745  gsummatr01lem3  21266  mp2pm2mplem4  21417  fiinopn  21509  cnmptcom  22286  fgcl  22486  fmfnfmlem1  22562  fmco  22569  flffbas  22603  cnpflf2  22608  metcnp3  23150  tngngp3  23265  clmvscom  23694  cphsscph  23854  aalioulem2  24922  elntg2  26771  ausgrusgrb  26950  usgredg4  26999  nbgr1vtx  27140  uhgr0edg0rgrb  27356  uhgrwkspth  27536  usgr2wlkspth  27540  uspgrn2crct  27586  crctcshwlkn0  27599  wwlksnredwwlkn  27673  wwlksnextsurj  27678  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  frgrnbnb  28072  frgrwopreglem5  28100  frgrwopreglem5ALT  28101  cvati  30143  dmdbr5ati  30199  loop1cycl  32384  sat1el2xp  32626  dfon2lem3  33030  frr3g  33121  bj-peircestab  33888  bj-0int  34396  ptrecube  34907  fzmul  35031  zerdivemp1x  35240  psshepw  40183  ndmaovdistr  43455  ssfz12  43563  fzopredsuc  43572  smonoord  43580  elsetpreimafvbi  43600  iccpartltu  43634  iccpartgtl  43635  ichreuopeq  43684  elsprel  43686  lighneallem3  43821  odd2prm2  43932  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  bgoldbnnsum3prm  44018  ringcbasbas  44354  ringcbasbasALTV  44378  ply1mulgsumlem2  44490  ldepsnlinclem1  44609  ldepsnlinclem2  44610  nnolog2flm1  44699  blengt1fldiv2p1  44702