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  3708  ssprsseq  4776  preqsnd  4810  elpr2elpr  4820  disjxiun  5090  oprabidw  7383  oprabid  7384  elovmporab  7598  elovmporab1w  7599  elovmporab1  7600  mpoxopoveqd  8157  wfr3g  8255  oewordri  8513  fsuppunbi  9279  frr3g  9655  r1sdom  9673  updjud  9833  kmlem4  10051  kmlem12  10059  domtriomlem  10339  zorn2lem6  10398  axdclem  10416  wunr1om  10616  tskr1om  10664  zindd  12580  hash2pwpr  14389  fi1uzind  14420  swrdnd0  14571  pfxccatin12  14646  repsdf2  14691  2cshwcshw  14738  cshwcshid  14740  fprodmodd  15910  alzdvds  16237  pwp1fsum  16308  lcmfdvds  16559  prm23ge5  16733  cshwshashlem2  17014  0ringnnzr  20446  01eq0ringOLD  20452  ringcbasbas  20594  psgndiflemA  21544  mplcoe5lem  21980  gsummoncoe1  22229  gsummatr01lem3  22578  mp2pm2mplem4  22730  fiinopn  22822  cnmptcom  23599  fgcl  23799  fmfnfmlem1  23875  fmco  23882  flffbas  23916  cnpflf2  23921  metcnp3  24461  tngngp3  24577  clmvscom  25023  cphsscph  25184  aalioulem2  26274  elntg2  28970  ausgrusgrb  29150  usgredg4  29202  nbgr1vtx  29343  uhgr0edg0rgrb  29560  uhgrwkspth  29740  usgr2wlkspth  29744  uspgrn2crct  29793  crctcshwlkn0  29806  wwlksnredwwlkn  29880  wwlksnextsurj  29885  hashecclwwlkn1  30064  umgrhashecclwwlk  30065  frgrnbnb  30280  frgrwopreglem5  30308  frgrwopreglem5ALT  30309  cvati  32353  dmdbr5ati  32409  loop1cycl  35188  sat1el2xp  35430  antnest  35740  dfon2lem3  35834  bj-peircestab  36604  bj-0int  37152  ptrecube  37666  fzmul  37787  zerdivemp1x  37993  psshepw  43886  ndmaovdistr  47312  ssfz12  47419  fzopredsuc  47428  smonoord  47476  elsetpreimafvbi  47496  iccpartltu  47530  iccpartgtl  47531  ichreuopeq  47578  elsprel  47580  lighneallem3  47712  odd2prm2  47823  nnsum4primeseven  47905  nnsum4primesevenALTV  47906  bgoldbnnsum3prm  47909  clnbgrgrimlem  48038  grtrif1o  48047  grtriclwlk3  48050  gpgprismgr4cycllem7  48206  pgnbgreunbgr  48230  ringcbasbasALTV  48417  ply1mulgsumlem2  48493  ldepsnlinclem1  48611  ldepsnlinclem2  48612  nnolog2flm1  48696  blengt1fldiv2p1  48699