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 526  3imtr4d 541  sbciegft 1949  intab 2550  ordsucss 3059  ordunel 3074  tfinds 3151  elreldm 3327  fvelimab 3750  ssimaex 3753  eqfnfv 3782  fconstfv 3834  f1oweALT 3891  oawordeulem 4172  oaass 4179  omordi 4181  omord 4183  odi 4194  oen0 4197  oeordi 4198  oeordsuc 4205  ecopoprtrn 4295  pw2en 4426  mapenlem2 4470  nndomo 4500  suppr 4562  inf3lem6 4590  rankr1lem 4645  rankval3 4653  aceq3lem 4704  aceq5lem4 4710  cardlim 4823  ondomcard 4829  cardmin 4832  alephord 4847  cardaleph 4857  cardinfima 4863  ltrpq 5057  prub 5070  genpnnp 5080  reclem3pr 5130  mulcmpblnr 5155  mulgt0sr 5186  xrre2t 5543  infm3 6001  supxrbnd 6038  supxrgtmnf 6039  zextlet 6136  primet 6142  uzindOLD 6156  zbtwnre 6169  flget 6178  ceilet 6193  elioc2t 6322  elico2t 6323  elicc2t 6324  fzoptht 6434  elfzp1 6442  fzrevralt 6451  expgt0t 6520  expgt1t 6523  seq1ublem 6848  cau3i 6851  facdivt 6879  fsum1ps 6956  fsumsplit 6958  fsumcmpndx2 6980  clm4le 7019  climmullem8 7063  caucvglem5 7097  caucvglem6 7098  caucvg 7099  infpnlem1 7449  bastgt 7564  tgclt 7566  basgen2t 7581  opnssneib 7670  clslp 7689  bl2in 7783  blssopn 7807  opnuni 7808  lmnn 7873  metcnp4 7904  xplmi 7907  xplm 7909  iscms2lem4 7926  ubthlem4 8463  ubthlem5 8464  minveclem26 8501  sincosq2sgn 8622  sincosq3sgn 8623  sincosq4sgn 8624  efif1lem3 8647  normpyct 8934  ocsh 9072  ocorth 9080  ococss 9082  projlem26 9127  shsel2t 9201  cm2jt 9480  lnfncnbdt 9907  riesz1t 9913  leopaddt 9977  leopmulit 9978  hstlest 10068  stge1 10075  stle0 10076  ssmd2 10147  superpos 10189  chcv1t 10190  atoml2 10218  irredlem2 10226  atcvat3 10231  mdsymlem5 10242  mdsymlem6 10243  sumdmdi 10249  sumdmdlem2 10253  cnrsfin 10396  cnrscoa 10397  cnvhmpha 10412  cnvhmphb 10413  hmphtr 10418  homgrf 10574  cmpmon 10585

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