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  3701  ssprsseq  4769  preqsnd  4803  elpr2elpr  4813  disjxiun  5083  oprabidw  7391  oprabid  7392  elovmporab  7606  elovmporab1w  7607  elovmporab1  7608  mpoxopoveqd  8164  wfr3g  8262  oewordri  8521  fsuppunbi  9295  frr3g  9671  r1sdom  9689  updjud  9849  kmlem4  10067  kmlem12  10075  domtriomlem  10355  zorn2lem6  10414  axdclem  10432  wunr1om  10633  tskr1om  10681  zindd  12621  hash2pwpr  14429  fi1uzind  14460  swrdnd0  14611  pfxccatin12  14686  repsdf2  14731  2cshwcshw  14778  cshwcshid  14780  fprodmodd  15953  alzdvds  16280  pwp1fsum  16351  lcmfdvds  16602  prm23ge5  16777  cshwshashlem2  17058  0ringnnzr  20493  01eq0ringOLD  20499  ringcbasbas  20641  psgndiflemA  21591  mplcoe5lem  22027  gsummoncoe1  22283  gsummatr01lem3  22632  mp2pm2mplem4  22784  fiinopn  22876  cnmptcom  23653  fgcl  23853  fmfnfmlem1  23929  fmco  23936  flffbas  23970  cnpflf2  23975  metcnp3  24515  tngngp3  24631  clmvscom  25067  cphsscph  25228  aalioulem2  26310  elntg2  29068  ausgrusgrb  29248  usgredg4  29300  nbgr1vtx  29441  uhgr0edg0rgrb  29658  uhgrwkspth  29838  usgr2wlkspth  29842  uspgrn2crct  29891  crctcshwlkn0  29904  wwlksnredwwlkn  29978  wwlksnextsurj  29983  hashecclwwlkn1  30162  umgrhashecclwwlk  30163  frgrnbnb  30378  frgrwopreglem5  30406  frgrwopreglem5ALT  30407  cvati  32452  dmdbr5ati  32508  loop1cycl  35335  sat1el2xp  35577  antnest  35887  dfon2lem3  35981  bj-peircestab  36831  bj-0int  37429  ptrecube  37955  fzmul  38076  zerdivemp1x  38282  psshepw  44233  ndmaovdistr  47667  ssfz12  47774  fzopredsuc  47784  smonoord  47837  elsetpreimafvbi  47863  iccpartltu  47897  iccpartgtl  47898  ichreuopeq  47945  elsprel  47947  lighneallem3  48082  odd2prm2  48206  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  bgoldbnnsum3prm  48292  clnbgrgrimlem  48421  grtrif1o  48430  grtriclwlk3  48433  gpgprismgr4cycllem7  48589  pgnbgreunbgr  48613  ringcbasbasALTV  48800  ply1mulgsumlem2  48875  ldepsnlinclem1  48993  ldepsnlinclem2  48994  nnolog2flm1  49078  blengt1fldiv2p1  49081