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.35OLD  3110  2rmorex  3751  ssprsseq  4829  preqsnd  4860  elpr2elpr  4870  disjxiun  5146  oprabidw  7440  oprabid  7441  elovmporab  7652  elovmporab1w  7653  elovmporab1  7654  mpoxopoveqd  8206  wfr3g  8307  oewordri  8592  fsuppunbi  9384  frr3g  9751  r1sdom  9769  updjud  9929  pr2neOLD  10000  kmlem4  10148  kmlem12  10156  domtriomlem  10437  zorn2lem6  10496  axdclem  10514  wunr1om  10714  tskr1om  10762  zindd  12663  hash2pwpr  14437  fi1uzind  14458  swrdnd0  14607  pfxccatin12  14683  repsdf2  14728  2cshwcshw  14776  cshwcshid  14778  fprodmodd  15941  alzdvds  16263  pwp1fsum  16334  lcmfdvds  16579  prm23ge5  16748  cshwshashlem2  17030  0ringnnzr  20302  01eq0ringOLD  20306  psgndiflemA  21154  mplcoe5lem  21594  gsummoncoe1  21828  gsummatr01lem3  22159  mp2pm2mplem4  22311  fiinopn  22403  cnmptcom  23182  fgcl  23382  fmfnfmlem1  23458  fmco  23465  flffbas  23499  cnpflf2  23504  metcnp3  24049  tngngp3  24173  clmvscom  24606  cphsscph  24768  aalioulem2  25846  elntg2  28243  ausgrusgrb  28425  usgredg4  28474  nbgr1vtx  28615  uhgr0edg0rgrb  28831  uhgrwkspth  29012  usgr2wlkspth  29016  uspgrn2crct  29062  crctcshwlkn0  29075  wwlksnredwwlkn  29149  wwlksnextsurj  29154  hashecclwwlkn1  29330  umgrhashecclwwlk  29331  frgrnbnb  29546  frgrwopreglem5  29574  frgrwopreglem5ALT  29575  cvati  31619  dmdbr5ati  31675  loop1cycl  34128  sat1el2xp  34370  dfon2lem3  34757  bj-peircestab  35429  bj-0int  35982  ptrecube  36488  fzmul  36609  zerdivemp1x  36815  psshepw  42539  ndmaovdistr  45915  ssfz12  46022  fzopredsuc  46031  smonoord  46039  elsetpreimafvbi  46059  iccpartltu  46093  iccpartgtl  46094  ichreuopeq  46141  elsprel  46143  lighneallem3  46275  odd2prm2  46386  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  bgoldbnnsum3prm  46472  ringcbasbas  46932  ringcbasbasALTV  46956  ply1mulgsumlem2  47068  ldepsnlinclem1  47186  ldepsnlinclem2  47187  nnolog2flm1  47276  blengt1fldiv2p1  47279