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  3711  ssprsseq  4780  preqsnd  4813  elpr2elpr  4823  disjxiun  5099  oprabidw  7452  oprabid  7453  elovmporab  7668  elovmporab1w  7669  elovmporab1  7670  mpoxopoveqd  8242  wfr3g  8341  oewordri  8605  fsuppunbi  9385  frr3g  9764  r1sdom  9785  updjud  10019  kmlem4  10236  kmlem12  10244  domtriomlem  10524  zorn2lem6  10583  axdclem  10601  wunr1om  10808  tskr1om  10856  zindd  12804  hash2pwpr  14625  fi1uzind  14656  swrdnd0  14812  pfxccatin12  14887  repsdf2  14934  2cshwcshw  14981  cshwcshid  14983  fprodmodd  16170  alzdvds  16496  pwp1fsum  16567  lcmfdvds  16823  prm23ge5  16999  cshwshashlem2  17280  0ringnnzr  20782  01eq0ringOLD  20788  ringcbasbas  20931  isfieldidl  21546  psgndiflemA  21913  mplcoe5lem  22354  gsummoncoe1  22632  gsummatr01lem3  22978  mp2pm2mplem4  23133  fiinopn  23225  cnmptcom  24003  fgcl  24203  fmfnfmlem1  24279  fmco  24286  flffbas  24320  cnpflf2  24325  metcnp3  24865  tngngp3  24981  clmvscom  25417  cphsscph  25578  aalioulem2  26666  elntg2  29569  ausgrusgrb  29752  usgredg4  29804  nbgr1vtx  29945  uhgr0edg0rgrb  30161  uhgrwkspth  30347  usgr2wlkspth  30351  uspgrn2crct  30403  crctcshwlkn0  30416  wwlksnredwwlkn  30490  wwlksnextsurj  30495  hashecclwwlkn1  30674  umgrhashecclwwlk  30675  loop1cycl  30750  frgrnbnb  30900  frgrwopreglem5  30928  frgrwopreglem5ALT  30929  cvati  32974  dmdbr5ati  33030  sat1el2xp  36231  antnest  36541  mirimanoffr  36547  dfon2lem3  36640  bj-peircestab  37513  bj-0int  38115  ptrecube  38632  fzmul  38769  zerdivemp1x  38975  psshepw  44882  ndmaovdistr  48371  ssfz12  48478  fzopredsuc  48488  smonoord  48541  elsetpreimafvbi  48567  iccpartltu  48601  iccpartgtl  48602  ichreuopeq  48649  elsprel  48651  lighneallem3  48786  odd2prm2  48910  nnsum4primeseven  48992  nnsum4primesevenALTV  48993  bgoldbnnsum3prm  48996  clnbgrgrimlem  49125  grtrif1o  49134  grtriclwlk3  49137  gpgprismgr4cycllem7  49293  pgnbgreunbgr  49317  ringcbasbasALTV  49503  ply1mulgsumlem2  49593  ldepsnlinclem1  49711  ldepsnlinclem2  49712  nnolog2flm1  49796  blengt1fldiv2p1  49799