Theorem sylibd 177

Description: A syllogism deduction.

Hypotheses

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

Assertion

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

Proof of Theorem sylibd

Step	Hyp	Ref	Expression
1		sylibd.1	. 2 |- (ph -> (ps -> ch))
2		sylibd.2	. . 3 |- (ph -> (ch <-> th))
3	2	biimpd 135	. 2 |- (ph -> (ch -> th))
4	1, 3	syld 27	1 |- (ph -> (ps -> th))

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

This theorem is referenced by:  bitrd 406  3imtr3d 420  bisbcdv 1468  rax4 1471  ordzsl 2366  fvopab2 2878  oaword2 3155  oaordex 3160  oen0 3165  nnmordi 3188  php3 3411  onomeneq 3414  suc11reg 3456  rankr1 3518  aceq3lem 3555  ac6lem 3575  cardne 3637  cardaleph 3690  ltexpq 3874  addclprlem1 3912  addclprlem2 3913  mulclprlem 3915  ltexprlem7 3942  prlem936b 3948  reclem4pr 3953  sqgt0sr 4009  addcan 4120  mulcan 4207  nnleltp1t 4448  uzind 4603  qbtwnre 4650  sqr2irr 4782  hial0 5058  hial2eqt 5060  chocuni 5179  shlej1t 5356  h1datom 5483  pjss2co 5634  pjnormss 5638  pjorthco 5639  pjclem4a 5652  pj3lem1 5658  pj3cor1 5661  stm1 5684  strlem1 5691  golem2 5705  mdbr2 5728  ssmd2 5735  atexch 5769  atcvatlem 5770

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