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  1300  19.30dc  1625  nf4r  1669  cbvexv1  1750  cbvexh  1753  equveli  1757  sbequilem  1836  sb5rf  1850  nfsbxy  1940  nfsbxyt  1941  sbcomxyyz  1970  dvelimALT  2008  dvelimfv  2009  dvelimor  2016  mo2n  2052  mo23  2065  2exeu  2116  bm1.1  2160  necon1idc  2398  sbhypf  2784  vtocl2  2790  vtocl3  2791  reu6  2924  rmo2ilem  3050  uneqin  3384  abn0r  3445  inelcm  3481  vdif0im  3486  difrab0eqim  3487  r19.3rm  3509  r19.9rmv  3512  difprsn1  3728  intminss  3865  disjnim  3989  bm1.3ii  4119  intexabim  4147  copsex2g  4240  opelopabt  4256  eusv2nf  4450  reusv3i  4453  onintrab2im  4511  ordtri2orexmid  4516  setindel  4531  onsucuni2  4557  ordtri2or2exmid  4564  zfregfr  4567  tfi  4575  mosubopt  4685  eqrelrel  4721  xpiindim  4757  opeliunxp2  4760  opelrn  4854  issref  5003  xpmlem  5041  rnxpid  5055  ssxpbm  5056  relcoi2  5151  unixpm  5156  cnviinm  5162  iotanul  5185  funimaexglem  5291  fvelrnb  5555  fvmptssdm  5592  fnfvrnss  5668  fressnfv  5695  fconstfvm  5726  f1mpt  5762  ovprc  5900  fo1stresm  6152  fo2ndresm  6153  spc2ed  6224  opeliunxp2f  6229  reldmtpos  6244  tfrlem5  6305  tfrlem9  6310  tfri2  6357  frecfcllem  6395  frecsuclem  6397  fvmptmap  6675  ixpiinm  6714  ixp0  6721  mptelixpg  6724  ener  6769  domtr  6775  unen  6806  xpf1o  6834  mapen  6836  ss1o0el1o  6902  cardval3ex  7174  distrnqg  7361  nqnq0pi  7412  nqnq0a  7428  nqnq0m  7429  distrnq0  7433  nqprloc  7519  ltexprlemopl  7575  ltexprlemopu  7577  recexre  8509  nn1suc  8909  msqznn  9324  nn0ind  9338  fnn0ind  9340  ublbneg  9584  qreccl  9613  fzo1fzo0n0  10151  elfzom1elp1fzo  10170  fzo0end  10191  fzind2  10207  flqeqceilz  10286  nnsinds  10411  nn0sinds  10412  ser0f  10483  hashfacen  10782  redivap  10849  imdivap  10856  cvg1nlemres  10960  sqrt0  10979  summodclem3  11354  fsump1i  11407  prodf1  11516  cos1bnd  11733  odd2np1  11843  opoe  11865  omoe  11866  opeo  11867  omeo  11868  dfgcd2  11980  gcdmultiplez  11987  dvdssq  11997  algfx  12017  odzval  12206  mul4sq  12357  setsfun0  12463  neipsm  13223  txbas  13327  elcncf1di  13635  reeff1o  13763  sincosq1lem  13815  sincosq2sgn  13817  sincosq4sgn  13819  lgsne0  14008  mul2sq  14021  bdbm1.3ii  14201