Theorem sylibr 200

Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition.

Hypotheses

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

Assertion

Ref	Expression
sylibr	|- (ph -> ch)

Proof of Theorem sylibr

Step	Hyp	Ref	Expression
1		sylibr.1	. 2 |- (ph -> ps)
2		sylibr.2	. . 3 |- (ch <-> ps)
3	2	biimpr 152	. 2 |- (ps -> ch)
4	1, 3	syl 10	1 |- (ph -> ch)

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

This theorem is referenced by:  3imtr4 219  orrd 233  jca 288  imp3a 361  impbid 514  con4bid 522  con2bid 524  pm5.74rd 586  ibd 592  oibabs 652  pm5.18 658  pm5.75 747  ecase2d 749  3mix1 813  3mix2 814  3jca 817  ecase23d 919  nicodraw 949  19.8a 1025  19.29 1067  19.39 1078  19.24 1079  19.34 1089  hbim1 1099  equs4 1146  a4ime 1156  a4imed 1157  sb2 1173  sbequ1 1174  sbn 1226  a4sbe 1238  ax11eq 1356  ax11el 1357  a12study 1371  mo 1386  eu2 1389  exmo 1409  2euex 1434  2mo 1440  2eu6 1447  bm1.1 1455  eqrdv 1466  abbid 1568  abbi2dv 1570  abbi1dv 1571  necon3bi 1599  necon2ai 1603  alral 1684  ra4e 1687  rgen2a 1691  r19.21ai 1704  r19.29 1748  elisset 1808  cgsex2g 1823  cgsex4g 1824  cla42egv 1855  cla43egv 1857  rcla4e 1863  ceqex 1877  elab3g 1893  mo2icl 1914  reu6 1922  elrabsf 1953  ssrdv 2060  eqssd 2069  3sstr4g 2092  syl5ss 2095  abssdv 2111  ssrabdv 2116  ss2rabdv 2117  rabss2 2119  pssn2lp 2137  psstr 2140  ssun1 2183  uneqin 2246  reuss2 2265  ne0i 2276  vss 2297  disjne 2305  minel 2314  disjsn 2431  disjsn2 2432  difsn 2455  sspr 2466  elunii 2498  uniss 2511  uniss2 2519  unidif 2520  ssunieq 2521  intmin 2543  intab 2550  iunss1 2564  ssiun2 2583  iunss2 2585  iunxdif2 2588  3brtr4g 2637  trin 2680  axnul2 2698  class2seteq 2725  notzfaus 2731  pwuni 2747  opprc3 2787  opthwiener 2796  ssopab2 2811  sotric 2851  so 2855  reucl2 2878  mouniss 2880  reusni 2883  rabsnt 2884  reuhyp 2895  eldifpw 2900  elpwun 2901  elpwunsn 2902  iunpw 2904  frirr 2914  fr0 2917  epfrc 2923  dfwe2 2925  wereu 2935  ordelord 2960  ordsseleq 2966  ordtri3or 2969  ordtri1 2970  orddisj 2975  ordon 2977  ssorduni 2983  onint0 2997  suceloni 3052  ordnbtwn 3053  ordsucss 3059  ordsucelsuc 3063  ordunisuc2 3105  ordzsl 3106  dflim3 3108  limuni3 3113  tfi 3116  omsson 3126  ordom 3131  omssnlim 3135  peano5 3143  xpsspw 3247  relop 3265  issetid 3269  cnvss 3280  opeldm 3303  dmcosseq 3349  relssres 3376  cotr 3420  dminss 3448  imainss 3449  xpnz 3452  cores 3485  relssdr 3499  funeu 3523  dffun7 3526  funco 3536  funun 3540  fununi 3549  funcnvuni 3550  funimaexg 3561  isarep2 3564  fnco 3581  fn0 3591  funimadisj 3592  zfrep6 3600  fnopabg 3601  fss 3620  fco 3621  funssxp 3623  fssres 3628  feu 3632  fcnvres 3633  fimacnvdisj 3634  fabexg 3638  f00 3642  fconst 3643  f1co 3652  fores 3666  foconst 3668  f1o2 3678  f1o3 3679  f1f1orn 3684  f1oun 3691  fo00 3700  fv3 3718  tz6.12-1 3721  fvelrn 3797  dff4 3801  dff2 3802  dffo4 3805  exfo 3807  fopab2 3808  ffnfv 3813  fsn 3819  abrexex 3845  f1ofv 3862  f1oiso 3889  iunon 3894  iinon 3895  tfrlem10 3905  tfr3 3911  tz7.44-3 3915  tz7.48lem 3940  tz7.48-1 3941  tz7.49 3944  tz7.49c 3945  abianfp 3947  eloprabg 3992  fnoprabg 3997  ndmoprass 4034  ndmoprdistr 4035  2ndconst 4081  curry1 4082  1stcof 4085  unielxp 4091  oawordeulem 4172  oalimcl 4178  omlimcl 4193  oeordi 4198  oelim2 4206  oaabslem 4235  omsmo 4241  erdisj 4270  ecelqsi 4276  ecopoprtrn 4295  th3qlem1 4298  mapval2 4319  fpm 4322  map0b 4327  mapsn 4329  mapss 4330  ixpf 4340  ixpexg 4342  ixpssmap 4347  relsdom 4356  en2d 4381  dom2d 4385  ssdomg 4389  pw2en 4426  sbthlem2 4428  sbthlem3 4429  sbthlem7 4433  sbthlem8 4434  fodomr 4463  mapenlem2 4470  mapdom2lem 4473  mapxpen 4475  mapunen 4482  limenpsi 4485  php2 4494  php3 4495  ominf 4508  pssnn 4513  ssfi 4515  unblem1 4517  unblem2 4518  unfilem3 4526  unfi2 4529  unifi2 4533  abfii2 4536  abfii3 4537  abfii4 4538  pwfilem 4544  pwfi 4545  supeu 4552  suppr 4562  supsnALT 4564  inf3lem3 4587  inf3lem6 4590  isfinite 4606  nnsdom 4607  infensuc 4610  trcl 4617  setind 4620  r1tr 4626  r1ord 4627  r1val1 4630  tz9.12lem1 4631  tz9.12lem3 4633  tz9.13 4635  rankon 4643  r1pw 4658  rankxplim3 4686  rankxpsuc 4687  scottex 4688  scott0 4689  aceq5 4712  aceq6a 4713  aceq6b 4714  ac6lem 4726  kmlem4 4740  kmlem6 4742  kmlem8 4744  kmlem13 4749  zorn2lem6 4765  zorn2lem7 4766  zorn 4769  fodom 4770  brdom3 4773  brdom5 4774  brdom4 4775  oncardval 4791  oncardon 4792  oncardid 4793  carden 4803  cardsn 4806  entri 4811  entri2 4812  cardsdomel 4824  ondomon 4828  ondomcard 4829  cardmin 4832  alephnbtwn 4840  alephval2 4874  alephval3 4875  cfub 4880  cflim 4881  cardcf 4883  cflecard 4884  cfsuc 4887  cfom 4888  addclpi 4992  mulclpi 4993  recmulpq 5042  prnmadd 5072  genpn0 5078  genpnnp 5080  genpcl 5083  1pr 5089  psslinpr 5107  prlem934 5111  ltexprlem1 5114  ltexprlem4 5117  ltexprlem5 5118  ltexprlem7 5120  reclem1pr 5128  reclem2pr 5129  reclem3pr 5130  mulgt0sr 5186  suppsr3 5196  axaddrcl 5244  axmulrcl 5246  axrnegex 5255  axcnre 5258  pre-axsup 5263  ltxrltt 5472  renepnft 5510  renemnft 5511  ssxr 5513  msqge0 5588  recextlem2 5656  mulnzcnopr 5671  nn1suc 5887  nnleltp1t 5901  nnsub 5903  lbreu 5992  infmxrcl 6033  nnnegz 6085  elnnz 6092  elnnz1 6102  msqznn 6143  uzind 6153  uzwo5OLD 6159  uzwo3lem1 6164  uzwo3lem2 6165  zmin 6167  flval3t 6182  flge0nn0t 6185  flge1nnt 6186  znq 6196  qaddclt 6207  qnegclt 6208  qmulclt 6209  qrecclt 6211  rpaddclt 6227  rpmulclt 6228  rpdivclt 6229  seq1f 6260  seq1f2 6261  ser1ft 6265  shftf 6288  ioossicc 6330  iccf 6334  eluzt 6358  uztrn 6360  eluzaddi 6368  eluzsubi 6369  uzind4 6382  elfzuzt 6420  elfznnt 6426  elfznn0t 6428  seqzvalt 6472  seqz1 6479  sqrlem5 6607  rpsqrclt 6645  sqr2irrlem1 6654  creur 6673  creui 6674  replimt 6692  absrpclt 6790  nn0absclt 6816  abssubne0t 6820  abs2dift 6839  seq1ublem 6848  cau3i 6851  climeu 7037  climcmplem 7073  ser1f0 7106  isumclimtf 7131  infcvgaux2 7155  mulc1cncf 7214  ivthlem7 7222  ivthlem7OLD 7231  efseq1ex 7248  efaddlem2 7281  efaddlem27 7306  efne0t 7311  efsubt 7313  reeftlclt 7322  ef01tllem1 7325  ef01tllem2 7326  absef01tllem 7328  eirrlem3 7332  reeff1 7350  efcnlem1 7359  efcn 7363  reeff1o 7368  acdc3lem 7428  acdc2lem2 7431  acdc5lem2 7434  acdclem 7436  infpn2 7452  infxpidmlem3 7497  infxpidmlem7 7501  infxpidmlem8 7502  infxpidmlem11 7505  infdif 7511  infmap2lem2 7522  eltopsp 7546  tgvalt 7558  tgclt 7566  subbas2 7587  subtop 7588  sn0top 7589  distop 7591  fctop 7592  cctop 7594  clscld 7625  elcls 7646  neips 7668  unnei 7676  lpval 7684  clslp 7689  idcn 7705  dnsconst 7727  bl2in 7783  opntop 7810  lpbl 7819  metcn 7828  tgioo 7854  lmcvgnns 7879  lmsslem 7887  lmfexlem1 7891  metelcls 7900  xplm 7909  xpcn 7910  iscms2 7928  lmcau 7930  cmsss 7931  bcthlem8 7940  bcthlem14 7946  bcthlem30 7962  isgrp 7975  grpfo 7977  grpideu 7987  grpinveu 7998  grpinvf 8014  resgrprnOLD 8031  issubg 8053  ablmul 8068  ringsn 8100  nvex 8169  isnv 8170  va1cnlem 8279  nmosetn0 8360  nmolb 8366  nmlno0lem 8385  isblo3i 8392  blocnilem 8395  blocni 8396  lnocni 8397  sspph 8446  ipblnfi 8447  ubthlem5 8464  ubthlem6 8465  ssphl 8549  htthlem11 8560  spwmo 8580  spweu 8581  cosh111lem1 8629  efif1lem5 8649  circcltOLD 8656  circgrp 8660  shftefif1olem 8661  shftefif1olemOLD 8662  eff1i 8665  axgroth3 8718  bcsALT 8967  hlimreu 9031  hlimeu 9032  chsscm 9033  hsn0elch 9041  hhsst 9056  ocsh 9072  occont 9076  occl 9097  projlem4 9105  projlem6 9107  projlem10 9111  projlem28 9129  projlem29 9130  pjthlem14 9147  pjtheu 9150  pjoc1 9179  choc0 9205  choc1 9206  shintcl 9208  ococint 9212  hsupval2t 9215  spanclt 9219  hsupclt 9222  hsupss 9224  chsupsn 9227  spanss 9233  chlejb1 9314  chabs2t 9355  spanun 9382  spansn 9396  spanunsn 9419  h1datom 9421  cmbr3 9460  cmbr4 9461  lecm 9462  osumlem5 9499  osum 9503  osumcor2 9507  nonbool 9513  5oalem1 9516  5oalem2 9517  5oalem4 9519  5oalem5 9520  3oalem2 9525  pjss2 9542  pjjs 9562  pjmf1 9578  hmopex 9719  nmoplbt 9748  unopf1ot 9756  cnvunopt 9758  unoplint 9760  counopt 9761  nmfnlbt 9764  adjvalvalt 9777  hmopadj2t 9781  hmoplint 9782  bralnfnt 9788  nmlnop0ALT 9835  lnopm 9840  nmopunt 9854  unopbdt 9855  hmopst 9860  hmopmt 9861  hmopcot 9863  nmcopexlem1 9866  nmcopexlem4 9869  nmcoplb 9873  bdophm 9877  lnopcon 9878  nmcfnexlem1 9895  nmcfnexlem4 9898  nmcfnlb 9902  lnfncon 9905  cnlnadjlem2 9916  cnlnadjlem3 9917  cnlnadjlem4 9918  cnlnadjlem5 9919  cnlnssadj 9928  adjbdlnt 9931  adjbdlnb 9932  adjlnopt 9934  branmfnt 9951  hmopidmch 9990  hmopidmpj 9991  pjss2co 10003  pjnormss 10007  pjssdif2 10013  pjinvar 10029  pjclem4 10037  pjc 10038  pjcmmul2 10040  pj3s 10045  strlem1 10087  strlem3a 10089  hstrlem3a 10097  mdsl1 10156  mdslmd3 10167  csmdsym 10169  mdexch 10170  h1dat 10184  shatomistic 10196  chpssat 10198  atoml 10217  irred 10229  mdsymlem6 10243  sumdmdi 10249  cmmd 10250  sumdmdlem2 10253  dmdbr5at 10255  dmdbr6at 10256  cdjreu 10264  cdj3 10273  lediv2itALT 10276  ghomgrpilem2 10291  cayleylem1 10316  intn3an1d 10328  intn3an2d 10329  intn3an3d 10330  faimpex 10339  uninqs 10342  difeqri2 10344  elo 10345  ficli 10368  cdrci 10381  bsi 10382  topnem 10394  homeofval 10403  hmeogrp 10425  homcard 10426  qusp 10430  oefil2 10441  neifil 10442  filintf 10443  fgsb 10444  efilcp 10445  fgsb2 10449  efilcp2 10450  cnfilca 10451  dtopcl 10459  t2t1 10460  dmse1 10467  iintlem1 10476  trnij 10481  imonclem 10583  ismonc 10584  hgrablkcard 10610

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