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  3090  2rmorex  3728  ssprsseq  4792  preqsnd  4826  elpr2elpr  4836  disjxiun  5107  oprabidw  7421  oprabid  7422  elovmporab  7638  elovmporab1w  7639  elovmporab1  7640  mpoxopoveqd  8203  wfr3g  8301  oewordri  8559  fsuppunbi  9347  frr3g  9716  r1sdom  9734  updjud  9894  pr2neOLD  9965  kmlem4  10114  kmlem12  10122  domtriomlem  10402  zorn2lem6  10461  axdclem  10479  wunr1om  10679  tskr1om  10727  zindd  12642  hash2pwpr  14448  fi1uzind  14479  swrdnd0  14629  pfxccatin12  14705  repsdf2  14750  2cshwcshw  14798  cshwcshid  14800  fprodmodd  15970  alzdvds  16297  pwp1fsum  16368  lcmfdvds  16619  prm23ge5  16793  cshwshashlem2  17074  0ringnnzr  20441  01eq0ringOLD  20447  ringcbasbas  20589  psgndiflemA  21517  mplcoe5lem  21953  gsummoncoe1  22202  gsummatr01lem3  22551  mp2pm2mplem4  22703  fiinopn  22795  cnmptcom  23572  fgcl  23772  fmfnfmlem1  23848  fmco  23855  flffbas  23889  cnpflf2  23894  metcnp3  24435  tngngp3  24551  clmvscom  24997  cphsscph  25158  aalioulem2  26248  elntg2  28919  ausgrusgrb  29099  usgredg4  29151  nbgr1vtx  29292  uhgr0edg0rgrb  29509  uhgrwkspth  29692  usgr2wlkspth  29696  uspgrn2crct  29745  crctcshwlkn0  29758  wwlksnredwwlkn  29832  wwlksnextsurj  29837  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  frgrnbnb  30229  frgrwopreglem5  30257  frgrwopreglem5ALT  30258  cvati  32302  dmdbr5ati  32358  loop1cycl  35131  sat1el2xp  35373  antnest  35683  dfon2lem3  35780  bj-peircestab  36548  bj-0int  37096  ptrecube  37621  fzmul  37742  zerdivemp1x  37948  psshepw  43784  ndmaovdistr  47212  ssfz12  47319  fzopredsuc  47328  smonoord  47376  elsetpreimafvbi  47396  iccpartltu  47430  iccpartgtl  47431  ichreuopeq  47478  elsprel  47480  lighneallem3  47612  odd2prm2  47723  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  bgoldbnnsum3prm  47809  clnbgrgrimlem  47937  grtrif1o  47945  grtriclwlk3  47948  gpgprismgr4cycllem7  48095  pgnbgreunbgr  48119  ringcbasbasALTV  48304  ply1mulgsumlem2  48380  ldepsnlinclem1  48498  ldepsnlinclem2  48499  nnolog2flm1  48583  blengt1fldiv2p1  48586