Theorem sylbir 176

Description: A mixed syllogism inference from a biconditional and an implication.

Hypotheses

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

Assertion

Ref	Expression
sylbir	|- (ph -> ch)

Proof of Theorem sylbir

Step	Hyp	Ref	Expression
1		sylbir.1	. . 3 |- (ps <-> ph)
2	1	biimpr 134	. 2 |- (ph -> ps)
3		sylbir.2	. 2 |- (ps -> ch)
4	2, 3	syl 12	1 |- (ph -> ch)

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

This theorem is referenced by:  3imtr3 191  exp 291  an42s 391  pm5.18 497  ecase3 559  3exp 611  sbi2 885  mo 1020  mo2 1026  2exeu 1066  bm1.1 1088  vtocl2 1379  vtocl3 1380  vsbcint 1438  bm1.3ii 1481  inelcm 1742  difin0ss 1753  copsex2g 1903  onminsb 2264  onminesb 2265  onintss 2266  onintrab 2268  onnminsb 2271  onminex 2275  tfindsg2 2403  brelrn 2559  opelrn 2560  cotr 2625  cnvsym 2626  zfrep6 2744  tz6.12 2843  fnfvrnss 2893  fressnfv 2898  fconstfv 2903  f1owe 2943  tfrlem5 2953  tfrlem8 2956  tfrlem9 2957  tfr2 2963  rdgsucopab 2984  rdgsucopabn 2985  frsucopab 2992  tz7.48-2 2995  oprprc1 3019  oprssdm 3056  1st2val 3097  oaordi 3148  ener 3313  domtr 3320  snfi 3337  unen 3338  mapenlem1 3384  unblem1 3431  unfi 3441  inf3lem2 3465  inf3lem5 3468  r1tr 3498  tz9.12lem1 3503  rankel 3524  bndrank 3526  unbndrank 3527  aceq4 3557  ac5b 3574  ac6s2 3578  kmlem6 3585  kmlem8 3587  kmlem13 3592  cardonle 3629  sucxpdom 3652  cardsdomel 3658  cardmin 3666  alephon 3671  alephcard 3673  alephnbtwn 3674  alephsson 3699  cfub 3703  cflecard 3707  cfle 3708  cdadom1 3727  ltpiord 3809  indpi 3828  addcanpr 3946  reclem1pr 3950  suplem1pr 3955  supsrlem5 4023  mul0or 4210  letri 4306  peano5nn 4424  uzind 4603  sqrval 4729  sqr2irrlem1 4777  climunii 4883  znnen 4930  infxpidmlem7 4939  bcs 5101  hlimunii 5143  ocvalt 5161  omlsilem 5249  spanvalt 5300  dfchj3 5326  h1de2b 5459  h1de2ctlem 5460  pjoi0 5592  hatomistic 5755  chpssat 5756  mdsymlem3 5778  mdsym 5784

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