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  3712  ssprsseq  4786  preqsnd  4819  elpr2elpr  4829  disjxiun  5100  oprabidw  7449  oprabid  7450  elovmporab  7665  elovmporab1w  7666  elovmporab1  7667  mpoxopoveqd  8231  wfr3g  8330  oewordri  8594  fsuppunbi  9374  frr3g  9753  r1sdom  9774  updjud  10008  kmlem4  10225  kmlem12  10233  domtriomlem  10513  zorn2lem6  10572  axdclem  10590  wunr1om  10797  tskr1om  10845  zindd  12793  hash2pwpr  14614  fi1uzind  14645  swrdnd0  14800  pfxccatin12  14875  repsdf2  14922  2cshwcshw  14969  cshwcshid  14971  fprodmodd  16157  alzdvds  16483  pwp1fsum  16554  lcmfdvds  16810  prm23ge5  16986  cshwshashlem2  17267  0ringnnzr  20769  01eq0ringOLD  20775  ringcbasbas  20918  isfieldidl  21533  psgndiflemA  21900  mplcoe5lem  22341  gsummoncoe1  22619  gsummatr01lem3  22965  mp2pm2mplem4  23120  fiinopn  23212  cnmptcom  23990  fgcl  24190  fmfnfmlem1  24266  fmco  24273  flffbas  24307  cnpflf2  24312  metcnp3  24852  tngngp3  24968  clmvscom  25404  cphsscph  25565  aalioulem2  26653  elntg2  29556  ausgrusgrb  29739  usgredg4  29791  nbgr1vtx  29932  uhgr0edg0rgrb  30148  uhgrwkspth  30334  usgr2wlkspth  30338  uspgrn2crct  30390  crctcshwlkn0  30403  wwlksnredwwlkn  30477  wwlksnextsurj  30482  hashecclwwlkn1  30661  umgrhashecclwwlk  30662  loop1cycl  30737  frgrnbnb  30887  frgrwopreglem5  30915  frgrwopreglem5ALT  30916  cvati  32961  dmdbr5ati  33017  sat1el2xp  36123  antnest  36433  dfon2lem3  36527  bj-peircestab  37400  bj-0int  38002  ptrecube  38518  fzmul  38655  zerdivemp1x  38861  psshepw  44773  ndmaovdistr  48246  ssfz12  48353  fzopredsuc  48363  smonoord  48416  elsetpreimafvbi  48442  iccpartltu  48476  iccpartgtl  48477  ichreuopeq  48524  elsprel  48526  lighneallem3  48661  odd2prm2  48785  nnsum4primeseven  48867  nnsum4primesevenALTV  48868  bgoldbnnsum3prm  48871  clnbgrgrimlem  49000  grtrif1o  49009  grtriclwlk3  49012  gpgprismgr4cycllem7  49168  pgnbgreunbgr  49192  ringcbasbasALTV  49378  ply1mulgsumlem2  49468  ldepsnlinclem1  49586  ldepsnlinclem2  49587  nnolog2flm1  49671  blengt1fldiv2p1  49674