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 659  ecase3 751  3exp 831  3ori 883  sbi2 1231  sb5rf 1257  ax11eq 1361  ax11el 1362  a12lem1 1374  a12study 1376  mo 1391  mo2 1398  2exeu 1444  2mo 1445  bm1.1 1460  necon1bi 1606  necon1i 1607  necon4ai 1621  pm2.61ine 1631  vtocl2 1839  vtocl3 1840  reu3 1927  sbhypf 1935  sbhyp 1936  uneqin 2252  inelcm 2319  difin0ss 2328  iununi 2611  bm1.3ii 2701  copsex2g 2788  eldifpw 2905  onminsb 3004  onminesb 3005  onintss 3006  onintrab 3008  onnminsb 3011  onminex 3015  tfindsg2 3158  opelrn 3340  cotr 3428  cnvsym 3429  ssxpr 3467  zfrep6 3606  fnfvrnss 3821  fopabco 3823  fopabcos 3824  fressnfv 3829  fopabsn 3831  fconst5 3839  fconstfv 3840  f1owe 3896  tfrlem5 3906  tfrlem9 3910  tfr2 3916  rdgsucopab 3937  rdgsucopabn 3938  frsucopab 3945  tz7.48-2 3948  oprprc1 3975  oprssdm 4033  1st2val 4085  2nd2val 4086  oaordi 4170  oeordi 4204  fvopabf4 4330  ener 4397  domtr 4402  snfi 4419  unen 4420  mapenlem1 4475  mapdom2 4480  unblem1 4523  unfi 4534  abfii4 4544  fodomfi 4546  inf3lem2 4594  inf3lem5 4597  r1tr 4634  tz9.12lem1 4639  rankel 4660  bndrank 4662  unbndrank 4663  rankxplim3 4694  aceq4 4714  ac5b 4733  ac6s2 4738  kmlem6 4750  kmlem8 4752  kmlem9 4753  iundom 4792  cardonle 4802  sucxpdom 4826  cardsdomel 4832  cardmin 4840  alephon 4845  alephcard 4847  alephnbtwn 4848  alephsson 4874  alephfp 4880  cfub 4888  cardcf 4891  cflecard 4892  cfle 4893  cdadom1 4913  ltpiord 4995  indpi 5014  reclem1pr 5136  suplem1pr 5141  supsrlem5 5209  letri 5566  mul0or 5671  peano5nn 5882  dfnn2 5892  infmrcl 6024  peano5uz 6159  uzindOLD 6164  nn0ind 6168  uzind4i 6394  fznt 6433  seqzm1 6489  sqrval 6609  sqr2irrlem1 6662  abs1m 6849  seq1ublem 6856  seq1ub 6857  cau5i 6862  cvg3 6868  cvganz 6869  faclbnd4lem1 6893  bcpasc 6915  ser0mulc 7005  ser1mulc 7006  ser0cj 7011  clm4 7026  climunii 7043  climshft2 7051  climfnrcl 7056  climaddc 7076  climmulc 7077  climcmplem 7081  caucvglem5 7105  caucvg3a 7108  caucvg3lem 7110  infcvglem2 7165  geolimilem 7178  geoisum1c 7188  cncfval 7207  elcncf1d 7213  ivthlem9 7232  efcltlem1 7254  efseq0ex 7261  reefcl 7267  efcj 7286  efaddlem26 7313  ef1tllem 7331  eirrlem2 7339  eirrlem4 7341  eirrlem5 7342  absefm1le 7360  efcn 7371  reeff1o 7376  cos1bnd 7424  znnen 7453  infxpidmlem7 7509  eltopsp 7554  tpsex 7555  subbas 7594  ismet 7748  ismsg 7750  msflem 7753  blssex 7806  opnin 7821  caun0 7896  xplm 7925  isgrp 7991  isring 8093  ringi 8094  vci 8119  vsfval 8206  nmogtmnf 8378  siilem1 8455  siii 8457  ajmoi 8463  spwval3 8596  spwnex3 8597  pilem2 8610  sincosq1lem 8639  sincosq2sgn 8641  sincosq4sgn 8643  cosh111lem1 8648  logclt 8697  eflogt 8699  bcsALT 8985  hhcms 9011  hlimunii 9047  ocvalt 9092  omlsilem 9182  spanvalt 9237  dfchj3 9263  h1de2b 9415  h1de2bOLD 9416  h1de2ctlem 9417  hoco 9630  hosubeq0 9692  adjmo 9698  nmopgtmnf 9735  adjvalvalt 9800  nmcopext 9897  lnopcon 9901  nmcfnext 9926  lnfncon 9928  riesz4 9934  riesz1t 9936  riesz2t 9937  superpos 10218  hatomistic 10226  chpssat 10227  mdsymlem3 10269  mdsym 10275  ghomgrp 10324  cayleylem3 10345  uninqs 10378  fiv 10410  fgsb 10480  efilcp 10481  fgsb2 10485  efilcp2 10486  cnfilca 10487  algi 10540  hgralem 10642

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