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  3700  ssprsseq  4768  preqsnd  4802  elpr2elpr  4812  disjxiun  5082  oprabidw  7398  oprabid  7399  elovmporab  7613  elovmporab1w  7614  elovmporab1  7615  mpoxopoveqd  8171  wfr3g  8269  oewordri  8528  fsuppunbi  9302  frr3g  9680  r1sdom  9698  updjud  9858  kmlem4  10076  kmlem12  10084  domtriomlem  10364  zorn2lem6  10423  axdclem  10441  wunr1om  10642  tskr1om  10690  zindd  12630  hash2pwpr  14438  fi1uzind  14469  swrdnd0  14620  pfxccatin12  14695  repsdf2  14740  2cshwcshw  14787  cshwcshid  14789  fprodmodd  15962  alzdvds  16289  pwp1fsum  16360  lcmfdvds  16611  prm23ge5  16786  cshwshashlem2  17067  0ringnnzr  20502  01eq0ringOLD  20508  ringcbasbas  20650  psgndiflemA  21581  mplcoe5lem  22017  gsummoncoe1  22273  gsummatr01lem3  22622  mp2pm2mplem4  22774  fiinopn  22866  cnmptcom  23643  fgcl  23843  fmfnfmlem1  23919  fmco  23926  flffbas  23960  cnpflf2  23965  metcnp3  24505  tngngp3  24621  clmvscom  25057  cphsscph  25218  aalioulem2  26299  elntg2  29054  ausgrusgrb  29234  usgredg4  29286  nbgr1vtx  29427  uhgr0edg0rgrb  29643  uhgrwkspth  29823  usgr2wlkspth  29827  uspgrn2crct  29876  crctcshwlkn0  29889  wwlksnredwwlkn  29963  wwlksnextsurj  29968  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  frgrnbnb  30363  frgrwopreglem5  30391  frgrwopreglem5ALT  30392  cvati  32437  dmdbr5ati  32493  loop1cycl  35319  sat1el2xp  35561  antnest  35871  dfon2lem3  35965  bj-peircestab  36815  bj-0int  37413  ptrecube  37941  fzmul  38062  zerdivemp1x  38268  psshepw  44215  ndmaovdistr  47655  ssfz12  47762  fzopredsuc  47772  smonoord  47825  elsetpreimafvbi  47851  iccpartltu  47885  iccpartgtl  47886  ichreuopeq  47933  elsprel  47935  lighneallem3  48070  odd2prm2  48194  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  bgoldbnnsum3prm  48280  clnbgrgrimlem  48409  grtrif1o  48418  grtriclwlk3  48421  gpgprismgr4cycllem7  48577  pgnbgreunbgr  48601  ringcbasbasALTV  48788  ply1mulgsumlem2  48863  ldepsnlinclem1  48981  ldepsnlinclem2  48982  nnolog2flm1  49066  blengt1fldiv2p1  49069