Theorem sylibrd 179

Description: A syllogism deduction.

Hypotheses

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

Assertion

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

Proof of Theorem sylibrd

Step	Hyp	Ref	Expression
1		sylibrd.1	. 2 |- (ph -> (ps -> ch))
2		sylibrd.2	. . 3 |- (ph -> (th <-> ch))
3	2	biimprd 136	. 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  3imtr4d 421  ordsucss 2320  tfinds 2401  elreldm 2554  fnex 2740  cleqfv 2880  fconstfv 2903  f1oweOLD 2944  oawordeulem 3156  oaass 3163  omordi 3164  oen0 3165  nnmordi 3188  nnmord 3189  ecopoprtrn 3247  pw2en 3348  mapenlem2 3385  nndomo 3416  inf3lem6 3469  rankr1lem 3517  rankval3 3525  aceq3lem 3555  aceq5lem4 3561  cardlim 3657  ondomcard 3663  cardmin 3666  alephord 3680  cardaleph 3690  cardinfima 3696  ltrpq 3879  prub 3892  genpnnp 3902  reclem3pr 3952  mulcmpblnr 3977  mulgt0sr 4008  divge0 4392  uzind 4603  zbtwnre 4619  flgzt 4626  normpyct 5093  ocsh 5164  ocorth 5172  ococss 5174  projlem26 5218  shsel2t 5287  stge1 5679  stle0 5680  chcv1t 5751  atcvat3 5774  mdsymlem5 5780  mdsymlem6 5781  sumdmdi 5785

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