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:  imbibi  394  2rmorex  3715  ssprsseq  4780  preqsnd  4814  elpr2elpr  4824  disjxiun  5094  oprabidw  7421  oprabid  7422  elovmporab  7636  elovmporab1w  7637  elovmporab1  7638  mpoxopoveqd  8194  wfr3g  8293  oewordri  8555  fsuppunbi  9328  frr3g  9707  r1sdom  9725  updjud  9885  kmlem4  10103  kmlem12  10111  domtriomlem  10392  zorn2lem6  10451  axdclem  10469  wunr1om  10670  tskr1om  10718  zindd  12667  hash2pwpr  14482  fi1uzind  14513  swrdnd0  14664  pfxccatin12  14739  repsdf2  14784  2cshwcshw  14831  cshwcshid  14833  fprodmodd  16017  alzdvds  16344  pwp1fsum  16415  lcmfdvds  16666  prm23ge5  16841  cshwshashlem2  17122  0ringnnzr  20561  01eq0ringOLD  20567  ringcbasbas  20709  psgndiflemA  21640  mplcoe5lem  22079  gsummoncoe1  22358  gsummatr01lem3  22704  mp2pm2mplem4  22856  fiinopn  22948  cnmptcom  23725  fgcl  23925  fmfnfmlem1  24001  fmco  24008  flffbas  24042  cnpflf2  24047  metcnp3  24587  tngngp3  24703  clmvscom  25139  cphsscph  25300  aalioulem2  26384  elntg2  29142  ausgrusgrb  29322  usgredg4  29374  nbgr1vtx  29515  uhgr0edg0rgrb  29731  uhgrwkspth  29911  usgr2wlkspth  29915  uspgrn2crct  29964  crctcshwlkn0  29977  wwlksnredwwlkn  30051  wwlksnextsurj  30056  hashecclwwlkn1  30235  umgrhashecclwwlk  30236  frgrnbnb  30451  frgrwopreglem5  30479  frgrwopreglem5ALT  30480  cvati  32525  dmdbr5ati  32581  loop1cycl  35447  sat1el2xp  35689  antnest  35999  dfon2lem3  36093  bj-peircestab  36953  bj-0int  37551  ptrecube  38079  fzmul  38200  zerdivemp1x  38406  psshepw  44324  ndmaovdistr  47761  ssfz12  47868  fzopredsuc  47878  smonoord  47931  elsetpreimafvbi  47957  iccpartltu  47991  iccpartgtl  47992  ichreuopeq  48039  elsprel  48041  lighneallem3  48176  odd2prm2  48300  nnsum4primeseven  48382  nnsum4primesevenALTV  48383  bgoldbnnsum3prm  48386  clnbgrgrimlem  48515  grtrif1o  48524  grtriclwlk3  48527  gpgprismgr4cycllem7  48683  pgnbgreunbgr  48707  ringcbasbasALTV  48894  ply1mulgsumlem2  48969  ldepsnlinclem1  49087  ldepsnlinclem2  49088  nnolog2flm1  49172  blengt1fldiv2p1  49175