Theorem sylibrd 204

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 154	. 2 |- (ph -> (ch -> th))
4	1, 3	syld 27	1 |- (ph -> (ps -> th))

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

This theorem is referenced by:  bitrd 528  3imtr4d 543  sbciegft 1959  intab 2560  ordsucss 3069  ordunel 3084  tfinds 3161  elreldm 3338  fvelimab 3765  ssimaex 3768  eqfnfv 3797  fconstfv 3849  f1oweALT 3906  oawordeulem 4188  oaass 4195  omordi 4197  omord 4199  odi 4210  oen0 4213  oeordi 4214  oeordsuc 4221  ecopoprtrn 4311  pw2en 4446  mapenlem2 4490  nndomo 4521  suppr 4590  inf3lem6 4618  rankr1lem 4673  rankval3 4681  aceq3lem 4732  aceq5lem4 4738  cardlim 4851  ondomcard 4857  cardmin 4860  alephord 4875  cardaleph 4885  cardinfima 4891  ltrpq 5085  prub 5098  genpnnp 5108  reclem3pr 5158  mulcmpblnr 5183  mulgt0sr 5214  xrre2t 5570  leltaddt 5646  infm3 6054  supxrbnd 6091  supxrgtmnf 6092  zextlet 6189  primet 6195  uzindOLD 6208  zbtwnre 6221  flget 6233  ceilet 6250  elioc2t 6390  elico2t 6391  elicc2t 6392  fzoptht 6502  elfzp1 6510  fzrevralt 6519  expgt0t 6589  expgt1t 6592  seq1ublem 6911  cau3i 6914  facdivt 6942  fsum1ps 7018  fsumsplit 7020  fsumcmpndx2 7042  clm4le 7081  climmullem8 7127  caucvglem5 7161  caucvglem6 7162  caucvg 7163  infpnlem1 7506  bastgt 7622  tgclt 7624  basgen2t 7639  opnssneib 7729  clslp 7748  bl2in 7843  blssopn 7867  opnuni 7868  lmnn 7935  metcnp4 7970  xplmi 7973  xplm 7975  iscms2lem4 7992  lnon0 8458  ubthlem4 8532  ubthlem5 8533  minveclem26 8570  spwpr3OLD 8662  sincosq2sgn 8705  sincosq3sgn 8706  sincosq4sgn 8707  efif1lem3 8732  normpyct 9013  ocsh 9156  ocorth 9164  ococss 9166  projlem26 9211  shsel2t 9286  cm2jt 9563  lnfncnbdt 9992  riesz1t 9998  leopaddt 10065  leopmulit 10066  hstlest 10158  stge1 10165  stle0 10166  dmdbr5 10235  ssmd2 10239  superpos 10281  chcv1t 10282  atoml2 10310  irredlem2 10318  atcvat3 10323  mdsymlem5 10334  mdsymlem6 10335  sumdmdi 10342  sumdmdlem2 10346  cnrsfin 10509  cnrscoa 10510  cnvhmpha 10525  cnvhmphb 10526  hmphtr 10531  homgrf 10730  cmpmon 10743

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