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 2855  nordeq 2962  nsuceq0 3048  onsucuni2 3086  tz6.12c 3731  tz7.48-1 3947  tz7.49 3950  oawordexr 4180  oewordi 4208  ecoptocl 4293  mapsn 4335  eqeng 4379  pw2en 4432  suc11reg 4585  inf3lem6 4598  rankc2 4686  zorn2lem4 4771  distrlem4pr 5110  1re 5415  lemul1it 5801  lemul1itOLD 5802  lt0nnn0 6071  recnzt 6146  om2uzran 6245  expge0t 6530  expge1t 6532  expwordit 6542  facdivt 6887  cvgcmpub 7129  ruclem33 7493  ruclem35 7495  iscld3 7645  isopn3 7647  cncnplem4 7727  cnconst 7730  ghgrpilem2 8086  efif1lem5 8668  hhssnv 9073  chocuni 9111  pjeqt 9180  h1dn0 9413  spansneleqi 9431  stm1 10108  mdbr2 10161  mdsl2 10186  sumdmdlem 10281  dmdbr6at 10285  ghomgrpilem2 10320

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