Theorem sylbi 187

Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
sylbi.1	⊢ (φ ↔ ψ)
sylbi.2	⊢ (ψ → χ)

Assertion

Ref	Expression
sylbi	⊢ (φ → χ)

Proof of Theorem sylbi

Step	Hyp	Ref	Expression
1		sylbi.1	. . 3 ⊢ (φ ↔ ψ)
2	1	biimpi 186	. 2 ⊢ (φ → ψ)
3		sylbi.2	. 2 ⊢ (ψ → χ)
4	2, 3	syl 15	1 ⊢ (φ → χ)

Syntax hints:   → wi 4   ↔ wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  bi2  189  3imtr4i  257  sylnbi  297  imp  418  an12s  776  an32s  779  an4s  799  oibabs  851  3simpb  953  3simpc  954  3imp  1145  3com12  1155  3com13  1156  syl3anb  1225  19.33b  1608  exintrbi  1613  ax17e  1618  spimfw  1646  a6e  1751  nfr  1761  19.9t  1779  nfnd  1791  nfndOLD  1792  equs5e  1888  exdistrf  1971  equvini  1987  equveli  1988  ax10-16  2190  euex  2227  eumo0  2228  mopick  2266  2euex  2276  2mo  2282  2eu3  2286  exists2  2294  eqcoms  2356  eleq2s  2445  nfcr  2481  necon3bi  2557  necon1ai  2558  necon2ai  2561  pm2.61ne  2591  pm2.61ine  2592  rexex  2673  rsp  2674  ralim  2685  r19.36av  2759  r19.37  2760  r19.44av  2767  r19.45av  2768  gencl  2887  gencbvex  2901  vtoclgf  2913  pm13.183  2979  mo2icl  3015  mob2  3016  reu3  3026  rmoim  3035  2reuswap  3038  sbcex  3055  ra5  3130  sseq1  3292  unineq  3505  dfrab3ss  3533  reldisj  3594  disjel  3597  pssdif  3612  difin0ss  3616  uneqdifeq  3638  r19.2z  3639  r19.3rz  3641  r19.3rzv  3643  ralidm  3653  ifnefalse  3670  ifbi  3679  nelpri  3754  difprsn2  3848  diftpsn3  3849  pwpw0  3855  ssunsn2  3865  snsssn  3873  pwsnALT  3882  intmin4  3955  dfiin2g  4000  iinss2  4018  unipw  4117  pwadjoin  4119  preqr2  4125  preq12b  4127  opkthg  4131  pw10  4161  pw10b  4166  pw1disj  4167  pw1ss  4169  sikss1c1c  4267  opkelimagekg  4271  ins2kss  4279  ins3kss  4280  cokrelk  4284  eqpw1uni  4330  pw1eqadj  4332  euabex  4334  iotauni  4351  iota1  4353  iota4  4357  reiotacl2  4363  dfiota4  4372  0nelsuc  4400  nndisjeq  4429  snfi  4431  lefinlteq  4463  ssfin  4470  tfinprop  4489  evenoddnnnul  4514  evenodddisj  4516  sfin112  4529  sfintfin  4532  sfinltfin  4535  sfin111  4536  spfinsfincl  4539  vfinspnn  4541  vfinspsslem1  4550  copsexg  4607  ralxpf  4827  optocl  4838  breldm  4911  proj1eldm  4927  dmcoss  4971  xpnz  5045  xp11  5056  xpcan  5057  xpcan2  5058  dfco2a  5081  cores2  5091  dfxp2  5113  dffun8  5134  fununi  5160  imadif  5171  fneu  5187  ffoss  5314  f1o00  5317  fo00  5318  nfunsn  5353  fvun1  5379  fvimacnv  5403  unpreima  5408  inpreima  5409  respreima  5410  fvpr1  5449  1stfo  5505  2ndfo  5506  xpnedisj  5513  1st2nd2  5516  oprabid  5550  oprssdm  5612  fvmptss  5705  fvmptss2  5725  op1st2nd  5790  oqelins4  5794  addcfnex  5824  pw1fnf1o  5855  clos1nrel  5886  weds  5938  ecexr  5950  mapprc  6004  mapsspm  6021  mapsspw  6022  map0b  6024  map0  6025  ensymi  6036  entr  6038  idssen  6040  en0  6042  fundmen  6043  xpen  6055  enpw1  6062  enmap2  6068  enmap1  6074  enprmaplem3  6078  nenpw1pwlem2  6085  ncseqnc  6128  muccl  6132  muccom  6134  mucass  6135  1cnc  6139  muc0  6142  mucid1  6143  ncdisjeq  6148  tcdi  6164  sbthlem3  6205  addlec  6208  nc0le1  6216  dflec3  6221  nclenc  6222  lenc  6223  tc11  6228  taddc  6229  letc  6231  ce2le  6233  cet  6234  te0c  6237  ce0lenc1  6239  tlenc1c  6240  addcdi  6250  muc0or  6252  nchoicelem8  6296  nchoicelem12  6300  nchoicelem14  6302  frecxp  6314  scancan  6331