Theorem syl5cbi 207

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 206	. 2 |- (ph -> (th -> ch))
4	3	com12 11	1 |- (th -> (ph -> ch))

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

This theorem is referenced by:  sotric 2939  nordeq 2994  nsuceq0 3053  suctr 3055  onsucuni2 3188  xp11 3561  tz6.12c 3851  tz7.48-1 4257  tz7.49 4260  oawordexr 4326  oewordi 4354  ectocl 4443  ecoptocl 4444  mapsn 4486  eqeng 4533  pw2en 4587  suc11reg 4750  inf3lem6 4763  rankc2 4852  zorn2lem4 4937  distrlem4pr 5284  1re 5589  lemul1a 5981  lemul1aOLD 5982  lt0nnn0 6284  recnz 6362  flidz 6435  modid2 6472  om2uzrani 6663  expge0 6785  expge1 6787  expwordi 6800  facdiv 7145  cvgcmpubi 7389  ruclem33 7754  ruclem35 7756  iscld3 7905  isopn3 7907  cncnplem4 7987  cnconst 7990  ghgrpilem2 8375  efif1lem5 9006  hhssnv 9410  chocunii 9448  pjeq 9518  h1dn0 9751  spansneleqi 9768  stm1i 10451  mdbr2 10504  mdsl2i 10530  sumdmdlem 10627  dmdbr6ati 10632  ghomgrpilem2 10671  twsymr 10808  rcfpfillem6 11094  bsi2 11139  elfiun 11421  ordtypelem4 11430  ordtypelem6 11432  omsubinit 11451  opnbnd 11461  hscptsscld 11491  reconnlem4 11510  is2ndc2 11534  2ndcsb 11537  2ndc1stc 11538  topfneec2 11563  filssufillem 11655  rnelfm 11699  fmfnfmlem4 11703  fmfnfm 11704  fcluscnp 11730  fcluscomp 11733  tailmap 11759  tailfb 11762  filnetlem3 11765  filnetlem4 11766  filnetlem5 11767  fipreima 11848  geomcau 11914  totbndss 11993  ismtyhmeolem 12006  ismtybndlem 12008  heiborlem7 12017  heiborlem13 12023  heiborlem23 12033

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 145

Copyright terms: Public domain