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  3702  ssprsseq  4763  preqsnd  4797  elpr2elpr  4807  disjxiun  5076  oprabidw  7394  oprabid  7395  elovmporab  7609  elovmporab1w  7610  elovmporab1  7611  mpoxopoveqd  8168  wfr3g  8266  oewordri  8525  fsuppunbi  9299  frr3g  9678  r1sdom  9696  updjud  9856  kmlem4  10074  kmlem12  10082  domtriomlem  10362  zorn2lem6  10421  axdclem  10439  wunr1om  10640  tskr1om  10688  zindd  12628  hash2pwpr  14436  fi1uzind  14467  swrdnd0  14618  pfxccatin12  14693  repsdf2  14738  2cshwcshw  14785  cshwcshid  14787  fprodmodd  15960  alzdvds  16287  pwp1fsum  16358  lcmfdvds  16609  prm23ge5  16784  cshwshashlem2  17065  0ringnnzr  20504  01eq0ringOLD  20510  ringcbasbas  20652  psgndiflemA  21583  mplcoe5lem  22022  gsummoncoe1  22301  gsummatr01lem3  22647  mp2pm2mplem4  22799  fiinopn  22891  cnmptcom  23668  fgcl  23868  fmfnfmlem1  23944  fmco  23951  flffbas  23985  cnpflf2  23990  metcnp3  24530  tngngp3  24646  clmvscom  25082  cphsscph  25243  aalioulem2  26324  elntg2  29079  ausgrusgrb  29259  usgredg4  29311  nbgr1vtx  29452  uhgr0edg0rgrb  29668  uhgrwkspth  29848  usgr2wlkspth  29852  uspgrn2crct  29901  crctcshwlkn0  29914  wwlksnredwwlkn  29988  wwlksnextsurj  29993  hashecclwwlkn1  30172  umgrhashecclwwlk  30173  frgrnbnb  30388  frgrwopreglem5  30416  frgrwopreglem5ALT  30417  cvati  32462  dmdbr5ati  32518  loop1cycl  35372  sat1el2xp  35614  antnest  35924  dfon2lem3  36018  bj-peircestab  36868  bj-0int  37466  ptrecube  37994  fzmul  38115  zerdivemp1x  38321  psshepw  44239  ndmaovdistr  47677  ssfz12  47784  fzopredsuc  47794  smonoord  47847  elsetpreimafvbi  47873  iccpartltu  47907  iccpartgtl  47908  ichreuopeq  47955  elsprel  47957  lighneallem3  48092  odd2prm2  48216  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  bgoldbnnsum3prm  48302  clnbgrgrimlem  48431  grtrif1o  48440  grtriclwlk3  48443  gpgprismgr4cycllem7  48599  pgnbgreunbgr  48623  ringcbasbasALTV  48810  ply1mulgsumlem2  48885  ldepsnlinclem1  49003  ldepsnlinclem2  49004  nnolog2flm1  49088  blengt1fldiv2p1  49091