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  3693  ssprsseq  4718  elpr2elpr  4759  disjxiun  5027  oprabidw  7166  oprabid  7167  elovmporab  7371  elovmporab1w  7372  elovmporab1  7373  mpoxopoveqd  7870  wfr3g  7936  oewordri  8201  fsuppunbi  8838  r1sdom  9187  updjud  9347  pr2ne  9416  kmlem4  9564  kmlem12  9572  domtriomlem  9853  zorn2lem6  9912  axdclem  9930  wunr1om  10130  tskr1om  10178  zindd  12071  hash2pwpr  13830  fi1uzind  13851  swrdnd0  14010  pfxccatin12  14086  repsdf2  14131  2cshwcshw  14178  cshwcshid  14180  fprodmodd  15343  alzdvds  15662  pwp1fsum  15732  lcmfdvds  15976  prm23ge5  16142  cshwshashlem2  16422  0ringnnzr  20035  01eq0ring  20038  psgndiflemA  20290  mplcoe5lem  20707  gsummoncoe1  20933  gsummatr01lem3  21262  mp2pm2mplem4  21414  fiinopn  21506  cnmptcom  22283  fgcl  22483  fmfnfmlem1  22559  fmco  22566  flffbas  22600  cnpflf2  22605  metcnp3  23147  tngngp3  23262  clmvscom  23695  cphsscph  23855  aalioulem2  24929  elntg2  26779  ausgrusgrb  26958  usgredg4  27007  nbgr1vtx  27148  uhgr0edg0rgrb  27364  uhgrwkspth  27544  usgr2wlkspth  27548  uspgrn2crct  27594  crctcshwlkn0  27607  wwlksnredwwlkn  27681  wwlksnextsurj  27686  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  frgrnbnb  28078  frgrwopreglem5  28106  frgrwopreglem5ALT  28107  cvati  30149  dmdbr5ati  30205  loop1cycl  32497  sat1el2xp  32739  dfon2lem3  33143  frr3g  33234  bj-peircestab  34001  bj-0int  34516  ptrecube  35057  fzmul  35179  zerdivemp1x  35385  psshepw  40489  ndmaovdistr  43763  ssfz12  43871  fzopredsuc  43880  smonoord  43888  elsetpreimafvbi  43908  iccpartltu  43942  iccpartgtl  43943  ichreuopeq  43990  elsprel  43992  lighneallem3  44125  odd2prm2  44236  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  bgoldbnnsum3prm  44322  ringcbasbas  44658  ringcbasbasALTV  44682  ply1mulgsumlem2  44795  ldepsnlinclem1  44914  ldepsnlinclem2  44915  nnolog2flm1  45004  blengt1fldiv2p1  45007