Theorem sylbir 218

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

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

This theorem is referenced by:  3imtr3i 235  an42s 567  pm5.18 722  pm5.18OLD 723  ecase3 825  dn1 855  dn1OLD 856  3exp 1066  3ori 1157  meredith 1200  19.33b 1444  sbi2 1603  sb5rf 1633  sb5rfOLD 1634  ax11eq 1754  ax11el 1755  a12lem1 1767  a12study 1769  mo 1787  mo2 1795  2exeu 1850  2mo 1851  bm1.1 1870  necon1biOLD 2049  necon1i 2050  necon4aiOLD 2068  pm2.61ineOLD 2090  vtocl2 2340  vtocl2OLD 2341  vtocl3 2342  vtocl3OLD 2343  euind 2439  reu6 2443  reuind 2450  sbhypf 2452  uneqin 2845  uneqinOLD 2846  inelcm 2928  difin0ss 2939  unissint 3241  iununi 3331  iununiOLD 3332  bm1.3ii 3441  copsex2g 3539  onintss 3713  eufromeq2 3829  eufromeq3 3830  eufromeq6 3833  euobj1 3834  euobj2 3835  eldifpw 3854  onminsb 3879  onminesb 3880  onintrab 3882  onnminsb 3885  onminex 3888  onsucuni2 3914  tfindsg2 3945  eqrelrel 4085  opelrn 4192  cotrOLD 4303  cnvsymOLD 4305  ssxpb 4346  dmsn0el 4366  zfrep6 4545  dffv2 4734  fnfvrnss 4803  fopabco 4805  fopabcos 4806  fressnfv 4813  fopabsnOLD 4816  fconst5 4824  fconstfv 4825  f1owe 4882  oprprc1 4908  oprssdm 4975  fo1stres 5036  fo2ndres 5037  1st2val 5038  2nd2val 5039  iotanul 5098  tfrlem5 5123  tfrlem9 5127  tfr2 5133  rdgsucopab 5154  rdgsucopabn 5155  frsucopab 5162  tz7.48-2 5166  oaordi 5227  oeordi 5262  fvopabf4 5399  ener 5469  domtr 5474  snfi 5491  unen 5493  mapenlem1 5583  mapdom2 5588  unblem1 5633  unfi 5644  abfii4 5654  fodomfi 5656  ordtypelem7 5690  inf3lem2 5720  inf3lem5 5723  r1tr 5765  tz9.12lem1 5770  rankel 5791  bndrank 5793  unbndrank 5794  rankxplim3 5825  cardonle 5868  alephon 5876  infenomsub 5889  aceq4 5896  ac5b 5915  ac6s2 5920  kmlem6 5932  kmlem8 5934  kmlem9 5935  iundom 5974  unsnen 5985  sucxpdom 5998  cardsdomel 6004  cardmin 6012  alephcard 6015  alephnbtwn 6016  alephsson 6042  alephfp 6048  cfub 6056  cardcf 6059  cflecard 6060  cfle 6061  cdadom1 6083  ltpiord 6167  indpi 6186  reclem1pr 6308  suplem1pr 6313  supsrlem5 6381  letrii 6759  mul0ori 6882  peano5nni 7109  dfnn2 7119  infmrcl 7278  peano5uzi 7415  uzindOLD 7420  nn0ind 7424  uzind4i 7623  fzn 7663  seqzm1 7792  sqrval 7921  sqr2irrlem1 7974  abs1mi 8156  seq1ublem 8163  seq1ubi 8164  cau5ii 8169  cvg3i 8175  cvganz 8176  faclbnd4lem1 8200  bcpasci 8221  ser0mulci 8319  ser1mulci 8320  ser0cji 8325  clm4i 8340  climunii 8358  climshft2i 8366  climfnrcli 8371  climaddci 8392  climmulci 8393  climcmplem 8397  caucvglem5 8421  caucvg3ai 8424  caucvg3lem 8426  ser1f0i 8430  infcvglem2 8483  geolimilem 8497  geoisum1c 8507  cncfval 8526  elcncf1di 8532  ivthlem9 8551  efcltlem1 8566  efseq0ex 8573  reefcli 8579  efcji 8598  efaddlem26 8625  ef1tllem 8643  eirrlem2 8652  eirrlem4 8654  eirrlem5 8655  absefm1lei 8677  efcn 8688  reeff1o 8691  cos1bnd 8740  znnen 8771  infxpidmlem7 8827  eltopsp 8873  tpsex 8874  subbas 8914  ismet 9075  ismsg 9077  msflem 9080  blssex 9131  opnin 9146  caun0 9223  xplm 9253  isgrp 9321  isgalem 9449  isring 9465  ringi 9466  vci 9499  vsfval 9586  vacnlem5 9671  nmogtmnf 9772  siilem1 9852  siii 9854  ajmoi 9860  spwval3 9997  spwnex3 9998  pilem2 10021  sincosq1lem 10052  sincosq2sgn 10054  sincosq4sgn 10056  cosh111lem1 10068  logcl 10112  eflog 10114  fiv 10212  sfvlim 10296  fintopcomp 10333  usinuniop 10341  ismgm 10367  fora 10408  uznzr 10416  isdivrng 10417  bcsiALT 10679  hhcms 10705  hlimuniii 10741  ocval 10786  omlsilem 10877  spanval 10932  dfchj3 10958  h1de2bi 11110  h1de2ctlem 11111  hocoi 11327  hosubeq0i 11389  adjmo 11395  nmopgtmnf 11432  adjvalval 11498  nmcopex 11596  lnopconi 11600  nmcfnex 11625  lnfnconi 11627  riesz4i 11633  riesz1 11635  riesz2 11636  opsqrlem1 11711  superpos 11926  hatomistici 11934  chpssati 11935  mdsymlem3 11977  mdsymi 11983  bnj50OLD 12425  bnj142 12474  bnj134 12478  bnj577 12549  bnj945 12844  bnj962 12856  bnj1139 12937  bnj1359 13084  bnj1381 13098  bnj1459 13140  bnj123 13233  bnj557 13281  bnj578 13291  bnj605 13292  bnj849 13318  bnj964 13347  bnj978 13355  bnj1018 13378  bnj1020 13379  bnj1033 13384  bnj1398 13515  bnj1417 13530  bnj1501 13570  bnj1523 13577  fnn0ind 13611  fseq1cl 13619  ghomgrp 13633  cayleylem3 13643  ublbneg 13653  gcdcllem1 13718  gcdaddmlem 13734  algfx 13748  eucalg 13755  mulgcdlem4 13759  4nprm 13781  dfon2lem7 13855  dfon2lem8 13856  frsucopabn 13911  frxp 13951  poseq 13954  soseq 13955  wfrlem4 13960  wfrlem12 13968  wfrlem16 13972  wfr2 13974  tfrALTlem 13976  axdenselem4 14022  axdenselem5 14023  nocvxminlem 14028  nocvxmin 14029  axfelem5 14035  axfelem7 14037  bisym1 14243  fampany 14288  althalne 14329  uninqs 14340  difeqri2 14341  domintrefb 14367  ref4w 14370  inttr 14384  twsymr 14394  fixpc 14418  celsor 14443  cmprelid1 14445  fopab2g 14485  dstr 14516  nZdef 14527  preoref22 14570  dfps2 14634  pospos 14635  seqzp2 14716  svli2 14826  vri 14834  topindis 14859  inttop2 14863  top2ind 14897  top2usne 14898  subtopsin2 14907  topgele 14910  fgsb 14921  efilcp 14922  fgsb2 14925  efilcp2 14926  cnfilca 14927  rcfpfillem2 14929  fbaslim2 14936  limfillem1 14938  conttnf 14944  iscnp3 14946  topunfincomp 14957  clindistop 14962  istopgrp 14971  cntrsetlem 14999  algi 15074  issubcat 15193  cptarc 15242  tarsuc2 15245  tarsuc3 15246  intartar 15255  tartarmap 15265  vtarsuelt 15272  inttarcar 15278  finminlem 15367  elfiun 15369  ordtypelem7OLD 15381  infenomsubOLD 15398  ssntr 15405  opnnei 15417  hscptsscld 15434  cnconn 15444  fneint 15486  islocfin 15506  fcluscf 15612  fcluscnplem 15617  filnet 15645  fimax 15746  zornn0 15764  infmrlb 15765  fsumltisumi 15823  geomcau 15849  haustlmu 15906  totbndbnd 15944  heiborlem11 15965  heiborlem41 15995  exidresid 16032  pcohtpy 16083  pcopt 16084  pcoass 16085  isdivrng1 16109  isdivrng2 16111  ispridl2 16186  igenmin 16212  prtlem11 16268  prter3 16286  hgralem 16292  pm11.71 16354  iotavalsb 16398  sbiota1 16399  smoge 16454  undif3VD 16706  lubval 16804  glbval 16809  joinlem 16817  meetlem 16824  clatlem 16889  hl2atom 17053  ocvval 17207

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 164

Copyright terms: Public domain