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:  r19.35  3271  2rmorex  3689  ssprsseq  4758  preqsnd  4789  elpr2elpr  4799  disjxiun  5071  oprabidw  7306  oprabid  7307  elovmporab  7515  elovmporab1w  7516  elovmporab1  7517  mpoxopoveqd  8037  wfr3g  8138  oewordri  8423  fsuppunbi  9149  frr3g  9514  r1sdom  9532  updjud  9692  pr2ne  9761  kmlem4  9909  kmlem12  9917  domtriomlem  10198  zorn2lem6  10257  axdclem  10275  wunr1om  10475  tskr1om  10523  zindd  12421  hash2pwpr  14190  fi1uzind  14211  swrdnd0  14370  pfxccatin12  14446  repsdf2  14491  2cshwcshw  14538  cshwcshid  14540  fprodmodd  15707  alzdvds  16029  pwp1fsum  16100  lcmfdvds  16347  prm23ge5  16516  cshwshashlem2  16798  0ringnnzr  20540  01eq0ring  20543  psgndiflemA  20806  mplcoe5lem  21240  gsummoncoe1  21475  gsummatr01lem3  21806  mp2pm2mplem4  21958  fiinopn  22050  cnmptcom  22829  fgcl  23029  fmfnfmlem1  23105  fmco  23112  flffbas  23146  cnpflf2  23151  metcnp3  23696  tngngp3  23820  clmvscom  24253  cphsscph  24415  aalioulem2  25493  elntg2  27353  ausgrusgrb  27535  usgredg4  27584  nbgr1vtx  27725  uhgr0edg0rgrb  27941  uhgrwkspth  28123  usgr2wlkspth  28127  uspgrn2crct  28173  crctcshwlkn0  28186  wwlksnredwwlkn  28260  wwlksnextsurj  28265  hashecclwwlkn1  28441  umgrhashecclwwlk  28442  frgrnbnb  28657  frgrwopreglem5  28685  frgrwopreglem5ALT  28686  cvati  30728  dmdbr5ati  30784  loop1cycl  33099  sat1el2xp  33341  dfon2lem3  33761  bj-peircestab  34733  bj-0int  35272  ptrecube  35777  fzmul  35899  zerdivemp1x  36105  psshepw  41396  ndmaovdistr  44699  ssfz12  44806  fzopredsuc  44815  smonoord  44823  elsetpreimafvbi  44843  iccpartltu  44877  iccpartgtl  44878  ichreuopeq  44925  elsprel  44927  lighneallem3  45059  odd2prm2  45170  nnsum4primeseven  45252  nnsum4primesevenALTV  45253  bgoldbnnsum3prm  45256  ringcbasbas  45592  ringcbasbasALTV  45616  ply1mulgsumlem2  45728  ldepsnlinclem1  45846  ldepsnlinclem2  45847  nnolog2flm1  45936  blengt1fldiv2p1  45939