Theorem syl5cbi 209

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

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

This theorem is referenced by:  sotric 2857  nordeq 2964  nsuceq0 3050  onsucuni2 3088  tz6.12c 3737  tz7.48-1 3953  tz7.49 3956  oawordexr 4187  oewordi 4215  ecoptocl 4300  mapsn 4342  eqeng 4386  pw2en 4439  suc11reg 4592  inf3lem6 4605  rankc2 4693  zorn2lem4 4778  distrlem4pr 5117  1re 5422  lemul1it 5807  lemul1itOLD 5808  lt0nnn0 6077  recnzt 6152  om2uzran 6255  expge0t 6541  expge1t 6543  expwordit 6553  facdivt 6908  cvgcmpub 7156  ruclem33 7521  ruclem35 7523  iscld3 7674  isopn3 7676  cncnplem4 7756  cnconst 7759  ghgrpilem2 8119  efif1lem5 8713  hhssnv 9122  chocuni 9160  pjeqt 9230  h1dn0 9463  spansneleqi 9481  stm1 10161  mdbr2 10214  mdsl2 10240  sumdmdlem 10336  dmdbr6at 10341  ghomgrpilem2 10377  rcfpfillem6 10551

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 147

Copyright terms: Public domain