Theorem syl5cbi 226

Description: A mixed syllogism inference.

Hypotheses

Ref	Expression
syl5bi.1	|- (ph -> (ps <-> ch))
syl5bi.2	|- (th -> ps)

Assertion

Ref	Expression
syl5cbi	|- (th -> (ph -> ch))

Proof of Theorem syl5cbi

Step	Hyp	Ref	Expression
1		syl5bi.1	. . 3 |- (ph -> (ps <-> ch))
2		syl5bi.2	. . 3 |- (th -> ps)
3	1, 2	syl5bi 225	. 2 |- (ph -> (th -> ch))
4	3	com12 14	1 |- (th -> (ph -> ch))

Syntax hints:   -> wi 3   <-> wb 163

This theorem is referenced by:  sotric 3615  sotrieq 3616  nordeq 3677  nsuceq0 3749  suctr 3751  dfwe2 3861  onsucuni2OLD 3915  iss 4254  xp11 4347  tz6.12c 4697  tz7.48-1 5165  tz7.49 5168  oawordexr 5238  oewordi 5266  ectocl 5361  ecoptocl 5362  mapsn 5404  eqeng 5451  pw2en 5505  ordtypelem4 5687  ordtypelem6 5689  suc11reg 5710  inf3lem6 5724  rankc2 5817  omsubinit 5890  zorn2lem4 5953  distrlem4pr 6282  1re 6598  lemul1a 7019  lemul1aOLD 7020  lt0nnn0 7325  recnz 7403  flidz 7476  modid2 7513  om2uzrani 7711  expge0 7833  expge1 7835  expwordi 7848  facdiv 8194  cvgcmpubi 8446  ruclem33 8811  ruclem35 8813  iscld3 8971  isopn3 8973  cncnplem4 9054  cnconst 9057  ghgrpilem2 9442  efif1lem5 10088  fipreima 10175  hhssnv 10767  chocunii 10805  pjeq 10875  h1dn0 11108  spansneleqi 11125  stm1i 11815  mdbr2 11868  mdsl2i 11894  sumdmdlem 11990  dmdbr6ati 11995  ghomgrpilem2 13629  dvdsnegb 13672  coprm 13782  dfon2lem9 13857  trclss 13935  poseq 13954  axdenselem5 14023  axdenselem8 14026  axfelem10 14040  axfelem15 14045  axfelem16 14046  twsymr 14394  rcfpfillem6 14933  fbfgss2 14937  bsi2 14992  elfiun 15369  ordtypelem4OLD 15378  ordtypelem6OLD 15380  omsubinitOLD 15399  opnbnd 15409  hscptsscld 15434  reconnlem4 15449  is2ndc2 15473  2ndcsb 15476  2ndc1stc 15477  topfneec2 15502  filssufillem 15570  rnelfm 15593  fmfnfmlem4 15597  fmfnfm 15598  fcluscnp 15618  fcluscomp 15621  tailmap 15636  tailfb 15639  filnetlem3 15642  filnetlem4 15643  filnetlem5 15644  fipreimaOLD 15756  geomcau 15849  totbndss 15937  ismtyhmeolem 15950  ismtybndlem 15952  heiborlem7 15961  heiborlem13 15967  heiborlem23 15977  igenval2 16214  isfldidl 16216  erdisj3 16266  xrltneNEW 16434  posasymb 16776  pleval2 16785  pltval3 16787  plttr 16790  cvrnbtwn3 16993  cvrnbtwn4 16996  cvrcmp 16999  atnlt 17009  hlexchb 17035  atcvr0eq 17064  cvrat4 17076  ps-1 17078  osumcllem4 17367  pexmidlem1 17378

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164

Copyright terms: Public domain