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  3268  2rmorex  3684  ssprsseq  4755  preqsnd  4786  elpr2elpr  4796  disjxiun  5067  oprabidw  7286  oprabid  7287  elovmporab  7493  elovmporab1w  7494  elovmporab1  7495  mpoxopoveqd  8008  wfr3g  8109  oewordri  8385  fsuppunbi  9079  frr3g  9445  r1sdom  9463  updjud  9623  pr2ne  9692  kmlem4  9840  kmlem12  9848  domtriomlem  10129  zorn2lem6  10188  axdclem  10206  wunr1om  10406  tskr1om  10454  zindd  12351  hash2pwpr  14118  fi1uzind  14139  swrdnd0  14298  pfxccatin12  14374  repsdf2  14419  2cshwcshw  14466  cshwcshid  14468  fprodmodd  15635  alzdvds  15957  pwp1fsum  16028  lcmfdvds  16275  prm23ge5  16444  cshwshashlem2  16726  0ringnnzr  20453  01eq0ring  20456  psgndiflemA  20718  mplcoe5lem  21150  gsummoncoe1  21385  gsummatr01lem3  21714  mp2pm2mplem4  21866  fiinopn  21958  cnmptcom  22737  fgcl  22937  fmfnfmlem1  23013  fmco  23020  flffbas  23054  cnpflf2  23059  metcnp3  23602  tngngp3  23726  clmvscom  24159  cphsscph  24320  aalioulem2  25398  elntg2  27256  ausgrusgrb  27438  usgredg4  27487  nbgr1vtx  27628  uhgr0edg0rgrb  27844  uhgrwkspth  28024  usgr2wlkspth  28028  uspgrn2crct  28074  crctcshwlkn0  28087  wwlksnredwwlkn  28161  wwlksnextsurj  28166  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  frgrnbnb  28558  frgrwopreglem5  28586  frgrwopreglem5ALT  28587  cvati  30629  dmdbr5ati  30685  loop1cycl  32999  sat1el2xp  33241  dfon2lem3  33667  bj-peircestab  34660  bj-0int  35199  ptrecube  35704  fzmul  35826  zerdivemp1x  36032  psshepw  41285  ndmaovdistr  44586  ssfz12  44694  fzopredsuc  44703  smonoord  44711  elsetpreimafvbi  44731  iccpartltu  44765  iccpartgtl  44766  ichreuopeq  44813  elsprel  44815  lighneallem3  44947  odd2prm2  45058  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  bgoldbnnsum3prm  45144  ringcbasbas  45480  ringcbasbasALTV  45504  ply1mulgsumlem2  45616  ldepsnlinclem1  45734  ldepsnlinclem2  45735  nnolog2flm1  45824  blengt1fldiv2p1  45827