Theorem sylbir 135

Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
sylbir.1	⊢ (𝜓 ↔ 𝜑)
sylbir.2	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
sylbir	⊢ (𝜑 → 𝜒)

Proof of Theorem sylbir

Step	Hyp	Ref	Expression
1		sylbir.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	biimpri 133	. 2 ⊢ (𝜑 → 𝜓)
3		sylbir.2	. 2 ⊢ (𝜓 → 𝜒)
4	2, 3	syl 14	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr3i  200  3ori  1337  19.30dc  1676  nf4r  1719  cbvexv1  1801  cbvexh  1804  equveli  1808  sbequilem  1887  sb5rf  1901  nfsbxy  1998  nfsbxyt  1999  sbcomxyyz  2028  dvelimALT  2066  dvelimfv  2067  dvelimor  2074  mo2n  2110  mo23  2124  2exeu  2175  bm1.1  2219  necon1idc  2467  sbhypf  2866  vtocl2  2872  vtocl3  2873  reu6  3009  rmo2ilem  3136  rabssrabd  3329  uneqin  3476  abn0r  3537  inelcm  3573  vdif0im  3578  difrab0eqim  3579  r19.3rm  3602  r19.9rmv  3605  difprsn1  3838  intminss  3979  disjnim  4104  bm1.3ii  4236  intexabim  4269  copsex2g  4367  opelopabt  4385  eusv2nf  4582  reusv3i  4585  onintrab2im  4645  ordtri2orexmid  4650  setindel  4665  onsucuni2  4691  ordtri2or2exmid  4698  zfregfr  4701  tfi  4709  mosubopt  4820  eqrelrel  4856  xpiindim  4897  opeliunxp2  4900  opelrn  4996  issref  5150  xpmlem  5188  rnxpid  5202  ssxpbm  5203  relcoi2  5298  unixpm  5303  cnviinm  5309  iotanul  5333  iotaexab  5336  funimaexglem  5444  fvelrnb  5729  fvmptssdm  5767  fnfvrnss  5842  fressnfv  5876  fconstfvm  5907  f1mpt  5950  ovprc  6094  fvmpopr2d  6198  fo1stresm  6368  fo2ndresm  6369  spc2ed  6442  opeliunxp2f  6482  reldmtpos  6497  tfrlem5  6558  tfrlem9  6563  tfri2  6610  frecfcllem  6648  frecsuclem  6650  fvmptmap  6932  ixpiinm  6972  ixp0  6979  mptelixpg  6982  ener  7032  domtr  7038  unen  7071  xpf1o  7110  mapen  7112  ss1o0el1o  7186  cardval3ex  7494  pr2cv2  7506  distrnqg  7718  nqnq0pi  7769  nqnq0a  7785  nqnq0m  7786  distrnq0  7790  nqprloc  7876  ltexprlemopl  7932  ltexprlemopu  7934  recexre  8869  nn1suc  9273  msqznn  9696  nn0ind  9710  fnn0ind  9712  ublbneg  9963  qreccl  9992  fzo1fzo0n0  10544  elfzom1elp1fzo  10569  fzo0end  10590  fzind2  10607  flqeqceilz  10704  nnsinds  10831  nn0sinds  10832  ser0f  10920  hashfacen  11233  iswrddm0  11273  swrdlsw  11386  pfxn0  11405  swrdswrdlem  11421  pfxccatin12lem3  11449  pfxccat3  11451  pfxccat3a  11455  swrdccat3blem  11456  redivap  11584  imdivap  11591  cvg1nlemres  11695  sqrt0  11714  summodclem3  12091  fsump1i  12144  prodf1  12253  cos1bnd  12470  odd2np1  12584  opoe  12606  omoe  12607  opeo  12608  omeo  12609  dfgcd2  12735  gcdmultiplez  12742  dvdssq  12752  algfx  12774  odzval  12964  mul4sq  13117  ballotfilemsdom  13199  ballotfilemth  13225  setsfun0  13332  rmodislmod  14625  isridl  14778  neipsm  15145  txbas  15249  elcncf1di  15570  plyco  15750  reeff1o  15764  sincosq1lem  15816  sincosq2sgn  15818  sincosq4sgn  15820  lgsne0  16037  2lgslem1  16090  mul2sq  16115  lpvtx  16200  umgrislfupgrenlem  16251  umgrislfupgrdom  16252  uspgr2wlkeq  16486  wlklenvclwlk  16494  bdbm1.3ii  16787