Theorem syl6bi 187

Description: A mixed syllogism inference.

Hypotheses

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

Assertion

Ref	Expression
syl6bi	|- (ph -> (ps -> th))

Proof of Theorem syl6bi

Step	Hyp	Ref	Expression
1		syl6bi.1	. . 3 |- (ph -> (ps <-> ch))
2	1	biimpd 135	. 2 |- (ph -> (ps -> ch))
3		syl6bi.2	. 2 |- (ch -> th)
4	2, 3	syl6 23	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  2eu2 1068  zfrepclf 1477  disjpss 1738  rzal 1773  preq12b 1874  prel12 1875  opprc3 1908  opth2 1909  reuuni4 1959  frirr 2176  ordsseleq 2227  ordsson 2242  nsuceq0 2306  ordssun 2330  ordequn 2331  peano5 2394  opeldm 2534  elreldm 2554  funimass2 2713  fvco 2865  funopfv 2886  fconstfv 2903  oaordi 3148  oa00 3161  oalimcl 3162  nnmordi 3188  nnaordex 3191  nnawordex 3192  erth 3219  ecopoprtrn 3247  opthreg 3455  inf3lemd 3463  inf3lem2 3465  inf3lem6 3469  r1tr 3498  rankr1 3518  r1pwcl 3530  karden 3551  aceq5lem4 3561  kmlem2 3581  kmlem11 3590  carden 3638  addnidpi 3822  indpi 3828  ordpipq 3850  ltsopq 3869  addcanpr 3946  prlem936 3949  suplem1pr 3955  suplem2pr 3956  ltsrpr 3980  ltsosr 3997  sqgt0sr 4009  addcan 4120  mulcan 4207  leltnet 4287  ltlent 4288  ltnsymt 4294  lt2sq 4414  lt1nnn 4442  nnunb 4520  btwnz 4613  zqt 4632  alephexp1 4954  normgt0t 5078  ocorth 5172  ocin 5177  cvpsst 5717  cvnbtwnt 5718  mdi 5727  dmdi 5732  atcvat 5771  mdsymlem6 5781

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

This theorem depends on definitions:  df-bi 128

metamath.org