Theorem sylbir 201

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 152	. 2 |- (ph -> ps)
3		sylbir.2	. 2 |- (ps -> ch)
4	2, 3	syl 10	1 |- (ph -> ch)

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

This theorem is referenced by:  3imtr3 218  an42s 509  pm5.18 660  ecase3 752  3exp 832  3ori 885  sbi2 1233  sb5rf 1259  ax11eq 1363  ax11el 1364  a12lem1 1376  a12study 1378  mo 1393  mo2 1400  2exeu 1446  2mo 1447  bm1.1 1462  necon1bi 1609  necon1i 1610  necon4ai 1624  pm2.61ine 1634  vtocl2 1843  vtocl3 1844  reu3 1931  sbhypf 1939  sbhyp 1940  uneqin 2256  inelcm 2323  difin0ss 2332  iununi 2616  bm1.3ii 2706  copsex2g 2793  eldifpw 2910  onminsb 3009  onminesb 3010  onintss 3011  onintrab 3013  onnminsb 3016  onminex 3020  tfindsg2 3163  opelrn 3345  cotr 3436  cnvsym 3437  ssxpr 3475  zfrep6 3614  fnfvrnss 3830  fopabco 3832  fopabcos 3833  fressnfv 3838  fopabsn 3840  fconst5 3848  fconstfv 3849  f1owe 3905  tfrlem5 3915  tfrlem9 3919  tfr2 3925  rdgsucopab 3946  rdgsucopabn 3947  frsucopab 3954  tz7.48-2 3957  oprprc1 3984  oprssdm 4042  1st2val 4095  2nd2val 4096  oaordi 4180  oeordi 4214  fvopabf4 4340  ener 4410  domtr 4415  snfi 4432  snfiOLD 4433  unen 4434  mapenlem1 4489  mapdom2 4494  unblem1 4540  unfi 4551  unfiOLD 4552  abfii4OLD 4564  fodomfiOLD 4566  inf3lem2 4614  inf3lem5 4617  r1tr 4654  tz9.12lem1 4659  rankel 4680  bndrank 4682  unbndrank 4683  rankxplim3 4714  aceq4 4734  ac5b 4753  ac6s2 4758  kmlem6 4770  kmlem8 4772  kmlem9 4773  iundom 4812  cardonle 4822  sucxpdom 4846  cardsdomel 4852  cardmin 4860  alephon 4865  alephcard 4867  alephnbtwn 4868  alephsson 4894  alephfp 4900  cfub 4908  cardcf 4911  cflecard 4912  cfle 4913  cdadom1 4933  ltpiord 5015  indpi 5034  reclem1pr 5156  suplem1pr 5161  supsrlem5 5229  letri 5584  mul0or 5694  peano5nn 5926  dfnn2 5936  infmrcl 6069  peano5uz 6203  uzindOLD 6208  nn0ind 6212  uzind4i 6454  fznt 6493  seqzm1 6549  sqrval 6671  sqr2irrlem1 6724  abs1m 6904  seq1ublem 6911  seq1ub 6912  cau5i 6917  cvg3 6923  cvganz 6924  faclbnd4lem1 6948  bcpasc 6969  ser0mulc 7059  ser1mulc 7060  ser0cj 7065  clm4 7080  climunii 7098  climshft2 7106  climfnrcl 7111  climaddc 7132  climmulc 7133  climcmplem 7137  caucvglem5 7161  caucvg3a 7164  caucvg3lem 7166  infcvglem2 7222  geolimilem 7235  geoisum1c 7245  cncfval 7264  elcncf1d 7270  ivthlem9 7289  efcltlem1 7304  efseq0ex 7311  reefcl 7317  efcj 7336  efaddlem26 7363  ef1tllem 7381  eirrlem2 7390  eirrlem4 7392  eirrlem5 7393  absefm1le 7412  efcn 7423  reeff1o 7426  cos1bnd 7474  znnen 7502  infxpidmlem7 7558  eltopsp 7604  tpsex 7605  subbasOLD 7644  ismet 7798  ismsg 7800  msflem 7803  blssex 7854  opnin 7869  caun0 7945  xplm 7975  isgrp 8041  isring 8141  ringi 8142  vci 8167  vsfval 8254  nmogtmnf 8433  siilem1 8511  siii 8513  ajmoi 8519  spwval3 8654  spwnex3 8655  pilem2 8672  sincosq1lem 8703  sincosq2sgn 8705  sincosq4sgn 8707  cosh111lem1 8714  logclt 8758  eflogt 8760  bcsALT 9046  hhcms 9072  hlimunii 9108  ocvalt 9153  omlsilem 9244  spanvalt 9299  dfchj3 9325  h1de2b 9477  h1de2ctlem 9478  hoco 9690  hosubeq0 9752  adjmo 9758  nmopgtmnf 9795  adjvalvalt 9861  nmcopext 9959  lnopcon 9963  nmcfnext 9988  lnfncon 9990  riesz4 9996  riesz1t 9998  riesz2t 9999  superpos 10281  hatomistic 10289  chpssat 10290  mdsymlem3 10332  mdsym 10338  ghomgrp 10390  cayleylem3 10411  uninqs 10441  fiv 10482  fivOLD 10483  sfseqeq 10543  top2ind 10548  top2usne 10549  fgsb 10570  fgsbOLD 10571  efilcp 10572  efilcpOLD 10573  fgsb2 10580  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem2 10587  rcfpfillem2OLD 10588  sfvlim 10605  algi 10660  hgralem 10770

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