Theorem syl11 34

Description: A syllogism inference. Commuted form of an instance of syl 18. (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 18	. 2 ⊢ (𝜃 → (𝜓 → 𝜒))
4	3	com12 33	1 ⊢ (𝜓 → (𝜃 → 𝜒))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imbibi  396  2rmorex  3715  ssprsseq  4786  preqsnd  4819  elpr2elpr  4829  disjxiun  5105  oprabidw  7482  oprabid  7483  elovmporab  7699  elovmporab1w  7700  elovmporab1  7701  mpoxopoveqd  8276  wfr3g  8375  oewordri  8639  fsuppunbi  9418  frr3g  9797  r1sdom  9818  updjud  10052  kmlem4  10271  kmlem12  10279  domtriomlem  10559  zorn2lem6  10618  axdclem  10636  wunr1om  10843  tskr1om  10891  zindd  12840  hash2pwpr  14662  fi1uzind  14693  swrdnd0  14849  pfxccatin12  14924  repsdf2  14971  2cshwcshw  15018  cshwcshid  15020  fprodmodd  16208  alzdvds  16534  pwp1fsum  16605  lcmfdvds  16861  prm23ge5  17037  cshwshashlem2  17318  0ringnnzr  20827  01eq0ringOLD  20833  ringcbasbas  20976  isfieldidl  21591  psgndiflemA  21962  mplcoe5lem  22403  gsummoncoe1  22681  gsummatr01lem3  23027  mp2pm2mplem4  23182  fiinopn  23274  cnmptcom  24052  fgcl  24252  fmfnfmlem1  24328  fmco  24335  flffbas  24369  cnpflf2  24374  metcnp3  24914  tngngp3  25030  clmvscom  25466  cphsscph  25627  aalioulem2  26717  elntg2  29620  ausgrusgrb  29803  usgredg4  29855  nbgr1vtx  29996  uhgr0edg0rgrb  30212  uhgrwkspth  30398  usgr2wlkspth  30402  uspgrn2crct  30454  crctcshwlkn0  30467  wwlksnredwwlkn  30541  wwlksnextsurj  30546  hashecclwwlkn1  30725  umgrhashecclwwlk  30726  loop1cycl  30801  frgrnbnb  30951  frgrwopreglem5  30979  frgrwopreglem5ALT  30980  cvati  33025  dmdbr5ati  33081  sat1el2xp  36352  antnest  36662  mirimanoffr  36668  elpssmo  36673  dfon2lem3  36762  bj-peircestab  37635  bj-0int  38292  ptrecube  38806  fzmul  38941  zerdivemp1x  39147  psshepw  45049  ndmaovdistr  48550  ssfz12  48657  fzopredsuc  48667  smonoord  48720  elsetpreimafvbi  48746  iccpartltu  48780  iccpartgtl  48781  ichreuopeq  48828  elsprel  48830  lighneallem3  48965  odd2prm2  49089  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  bgoldbnnsum3prm  49175  clnbgrgrimlem  49304  grtrif1o  49313  grtriclwlk3  49316  gpgprismgr4cycllem7  49472  pgnbgreunbgr  49496  ringcbasbasALTV  49682  ply1mulgsumlem2  49830  ldepsnlinclem1  49948  ldepsnlinclem2  49949  nnolog2flm1  50033  blengt1fldiv2p1  50036