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  1336  19.30dc  1675  nf4r  1719  cbvexv1  1800  cbvexh  1803  equveli  1807  sbequilem  1886  sb5rf  1900  nfsbxy  1995  nfsbxyt  1996  sbcomxyyz  2025  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  mo2n  2107  mo23  2121  2exeu  2172  bm1.1  2216  necon1idc  2455  sbhypf  2853  vtocl2  2859  vtocl3  2860  reu6  2995  rmo2ilem  3122  uneqin  3458  abn0r  3519  inelcm  3555  vdif0im  3560  difrab0eqim  3561  r19.3rm  3583  r19.9rmv  3586  difprsn1  3812  intminss  3953  disjnim  4078  bm1.3ii  4210  intexabim  4242  copsex2g  4338  opelopabt  4356  eusv2nf  4553  reusv3i  4556  onintrab2im  4616  ordtri2orexmid  4621  setindel  4636  onsucuni2  4662  ordtri2or2exmid  4669  zfregfr  4672  tfi  4680  mosubopt  4791  eqrelrel  4827  xpiindim  4867  opeliunxp2  4870  opelrn  4966  issref  5119  xpmlem  5157  rnxpid  5171  ssxpbm  5172  relcoi2  5267  unixpm  5272  cnviinm  5278  iotanul  5302  iotaexab  5305  funimaexglem  5413  fvelrnb  5693  fvmptssdm  5731  fnfvrnss  5807  fressnfv  5840  fconstfvm  5871  f1mpt  5911  ovprc  6053  fvmpopr2d  6157  fo1stresm  6323  fo2ndresm  6324  spc2ed  6397  opeliunxp2f  6403  reldmtpos  6418  tfrlem5  6479  tfrlem9  6484  tfri2  6531  frecfcllem  6569  frecsuclem  6571  fvmptmap  6853  ixpiinm  6892  ixp0  6899  mptelixpg  6902  ener  6952  domtr  6958  unen  6990  xpf1o  7029  mapen  7031  ss1o0el1o  7104  cardval3ex  7388  pr2cv2  7400  distrnqg  7606  nqnq0pi  7657  nqnq0a  7673  nqnq0m  7674  distrnq0  7678  nqprloc  7764  ltexprlemopl  7820  ltexprlemopu  7822  recexre  8757  nn1suc  9161  msqznn  9579  nn0ind  9593  fnn0ind  9595  ublbneg  9846  qreccl  9875  fzo1fzo0n0  10421  elfzom1elp1fzo  10446  fzo0end  10467  fzind2  10484  flqeqceilz  10579  nnsinds  10706  nn0sinds  10707  ser0f  10795  hashfacen  11099  iswrddm0  11136  swrdlsw  11249  pfxn0  11268  swrdswrdlem  11284  pfxccatin12lem3  11312  pfxccat3  11314  pfxccat3a  11318  swrdccat3blem  11319  redivap  11434  imdivap  11441  cvg1nlemres  11545  sqrt0  11564  summodclem3  11940  fsump1i  11993  prodf1  12102  cos1bnd  12319  odd2np1  12433  opoe  12455  omoe  12456  opeo  12457  omeo  12458  dfgcd2  12584  gcdmultiplez  12591  dvdssq  12601  algfx  12623  odzval  12813  mul4sq  12966  setsfun0  13117  rmodislmod  14364  isridl  14517  neipsm  14877  txbas  14981  elcncf1di  15302  plyco  15482  reeff1o  15496  sincosq1lem  15548  sincosq2sgn  15550  sincosq4sgn  15552  lgsne0  15766  2lgslem1  15819  mul2sq  15844  lpvtx  15929  umgrislfupgrenlem  15980  umgrislfupgrdom  15981  uspgr2wlkeq  16215  wlklenvclwlk  16223  bdbm1.3ii  16486