Theorem sylbi 174

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

Hypotheses

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

Assertion

Ref	Expression
sylbi	|- (ph -> ch)

Proof of Theorem sylbi

Step	Hyp	Ref	Expression
1		sylbi.1	. . 3 |- (ph <-> ps)
2	1	biimp 133	. 2 |- (ph -> ps)
3		sylbi.2	. 2 |- (ps -> ch)
4	2, 3	syl 12	1 |- (ph -> ch)

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

This theorem is referenced by:  3imtr4 192  pm3.26 256  pm3.27 260  imp 277  ancoms 334  an1s 372  an1rs 373  an4s 390  pm2.85 439  ordi 452  pm5.18 497  ccase 562  3simpb 592  3simpc 593  3imp 608  3com13 615  a6e 688  19.9r 718  19.33b 771  eqvin.l1 851  sb6x 871  hbsb4t 906  euex 1021  eumo0 1022  mooran2 1050  mopick 1054  2euex 1061  2eu3 1069  exists2 1073  cleqcoms 1104  rexex 1242  ra4 1243  r19.20 1251  r19.22 1272  r19.23ai 1283  r19.36av 1299  r19.37av 1300  r19.44av 1305  r19.45av 1306  2reuswap 1341  elisset 1354  gencl 1365  vtoclgf 1382  cla4gf 1394  rcla4v 1402  mo2icl 1434  sbcie 1455  rax5 1472  zfrep3 1476  zfrep4 1479  sstr2 1510  pssn2lp 1571  ssnpss 1573  reuxfr 1580  unineq 1680  ssex 1700  pssnel 1752  difin0ss 1753  r19.2z 1766  r19.3rzv 1767  ralidm 1774  ifbi 1783  prprc 1839  snex 1859  rext 1862  moabex 1868  prer2 1873  preq12b 1874  nnullss 1880  exss 1881  pwpw0 1883  prex 1892  opth 1898  copsexg 1902  opprc1 1905  opprc3 1908  pwssun 1917  euuni 1954  reucl 1957  unipw 1960  intex 1986  iunconst 2000  ssiun 2018  iununi 2037  trss 2050  ssopab2 2119  solin 2145  so 2152  fri 2170  frc 2172  frirr 2176  fr2nr 2177  fr3nr 2178  onfr 2237  tfi 2244  tfis 2245  nlim0 2282  limord 2283  limuni 2284  elsuci 2289  sucprc 2297  onmindif2 2313  suceloni 2314  onsucmin 2323  ordsucelsuc 2324  ordssun 2330  ordequn 2331  ordsucun 2333  unon 2338  ordunisuc 2339  0elsuc 2340  onuninsuc 2356  onun 2358  nlimsuc 2363  orduninsuc 2365  limomss 2378  limom 2387  findsg 2398  tfindsg 2402  opelxpex 2445  brrelex 2446  ralxp 2456  optocl 2469  onxpdisj 2476  relss 2480  xpex 2488  breldm 2535  dmsnop 2547  elreldm 2554  dmco 2570  resabs1 2592  imasn 2616  cnvsym 2626  coi2 2666  funsn 2690  imadif 2714  f1ocnvb 2812  f1oco 2816  ffoss 2820  f1o00 2823  fvprc 2829  tz6.12-1 2842  fvopabgf 2874  fvopabnf 2875  abrexexlem1 2910  f1oweOLD 2944  canth 2945  tfrlem4 2952  tfrlem5 2953  tfrlem7 2955  tfrlem8 2956  tfrlem9 2957  rdgsucopabn 2985  frsuc 2991  tz7.48lem 2993  tz7.48-1 2994  abianfplem 2999  abianfp 3000  oprssdm 3056  ndmoprcom 3061  oaord 3149  nnacom 3175  nnmsucr 3182  erref 3212  erthi 3218  ereldm 3222  erdisj 3223  ecelqsdm 3235  ectocl 3238  ecoptocl 3239  brecop2 3243  ecopoprdm 3245  th3qlem1 3250  mapprc 3260  map0b 3267  map0 3268  idssen 3309  ener 3313  en0 3328  en1 3331  2dom 3332  snfi 3337  xpsnen 3339  xpdom2 3345  xpdom3 3347  pw2en 3348  sbthlem1 3349  sbthlem10 3358  domnsym 3365  domsdomtr 3374  mapdom1 3387  mapdom2 3389  mapxpen 3390  mapunen 3397  ssenen 3399  phplem4 3406  php 3409  0sdom1dom 3420  ominf 3423  pssnn 3428  ssnn 3429  unfi 3441  infcntss 3443  fiint 3445  sucprcreg 3451  inf0 3457  inf3lem1 3464  inf5 3472  dfom3 3477  trcl 3489  zfregs 3491  setind2 3493  r1tr 3498  r1val1 3502  tz9.12lem1 3503  tz9.12lem3 3505  rankr1 3518  rankel 3524  rankuni 3533  rankun 3535  rankr1id 3539  scottex 3541  scott0 3542  bnd2 3549  karden 3551  aceq4 3557  aceq5lem4 3561  aceq5 3563  aceq6b 3565  ac6lem 3575  kmlem2 3581  kmlem4 3583  kmlem11 3590  kmlem12 3591  weth 3602  zornlem6 3608  zornlem7 3609  zorn2 3612  hta 3619  sucdom 3648  unxpdomlem 3649  carduni 3664  cardiun 3665  cardcf 3706  cfsuc 3709  indpi 3828  prn0 3887  prpssnq 3888  1pr 3911  distrlem3pr 3923  prlem934b 3932  ltexprlem4 3939  reclem2pr 3951  mulcmpblnr 3977  recexsrlem 4006  map2psrpr 4014  suppsr3 4018  supsrlem2 4020  axsup 4088  subeq0 4163  redivcl 4274  addgegt0 4325  sqgt0 4343  nnind 4434  sup3 4511  cru 4529  elnnz1 4581  znegclt 4588  elnn0nn 4593  nn0ind 4612  qret 4631  qnegclt 4643  qrecclt 4646  om2uzran 4655  uzrdgval 4657  seqlem1 4662  seqsuclem 4669  discrlem3 4715  discrlem 4716  nnesq 4720  sqrlem6 4736  sqrlem16 4746  sqrth 4757  sqrcl 4758  sqrge0 4760  rere 4810  negre 4825  absnid 4851  facp1t 4873  ruclem33 4917  ruclem35 4919  xpnnen 4927  infxpidmlem4 4936  infxpidmlem7 4939  infxpidmlem12 4944  infmap2lem1 4951  infmap2 4953  alephexp1 4954  alephsuc3 4955  alephexp2 4956  hvsubeq0 5035  bcs 5101  chsscm 5147  chcmh 5148  hsn0elch 5155  projlem8 5200  projlem13 5205  shintcl 5294  spanvalt 5300  dfchj2 5325  sshjclt 5328  shsidm 5358  spanun 5450  h1de2 5458  spansn 5462  spanunsn 5482  cmbr3 5509  osumlem1 5530  osumlem2 5531  osumlem3 5532  spansncv 5542  5oalem7 5550  3oalem3 5554  pjss2 5571  pjssm 5572  pjorthco 5639  pjin2 5647  pjclem1 5649  pjclem2 5650  pjclem4a 5652  pj3lem1 5658  strlem1 5691  strlem3 5694  strlem4 5695  strlem5 5696  str 5698  stcltr1 5707  atn0 5743  atss 5744  atom1d 5750  shatomic 5753  chrelat2 5758

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