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  1334  19.30dc  1673  nf4r  1717  cbvexv1  1798  cbvexh  1801  equveli  1805  sbequilem  1884  sb5rf  1898  nfsbxy  1993  nfsbxyt  1994  sbcomxyyz  2023  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  mo2n  2105  mo23  2119  2exeu  2170  bm1.1  2214  necon1idc  2453  sbhypf  2851  vtocl2  2857  vtocl3  2858  reu6  2993  rmo2ilem  3120  uneqin  3456  abn0r  3517  inelcm  3553  vdif0im  3558  difrab0eqim  3559  r19.3rm  3581  r19.9rmv  3584  difprsn1  3810  intminss  3951  disjnim  4076  bm1.3ii  4208  intexabim  4240  copsex2g  4336  opelopabt  4354  eusv2nf  4551  reusv3i  4554  onintrab2im  4614  ordtri2orexmid  4619  setindel  4634  onsucuni2  4660  ordtri2or2exmid  4667  zfregfr  4670  tfi  4678  mosubopt  4789  eqrelrel  4825  xpiindim  4865  opeliunxp2  4868  opelrn  4964  issref  5117  xpmlem  5155  rnxpid  5169  ssxpbm  5170  relcoi2  5265  unixpm  5270  cnviinm  5276  iotanul  5300  iotaexab  5303  funimaexglem  5410  fvelrnb  5689  fvmptssdm  5727  fnfvrnss  5803  fressnfv  5836  fconstfvm  5867  f1mpt  5907  ovprc  6049  fvmpopr2d  6153  fo1stresm  6319  fo2ndresm  6320  spc2ed  6393  opeliunxp2f  6399  reldmtpos  6414  tfrlem5  6475  tfrlem9  6480  tfri2  6527  frecfcllem  6565  frecsuclem  6567  fvmptmap  6849  ixpiinm  6888  ixp0  6895  mptelixpg  6898  ener  6948  domtr  6954  unen  6986  xpf1o  7025  mapen  7027  ss1o0el1o  7098  cardval3ex  7380  pr2cv2  7392  distrnqg  7597  nqnq0pi  7648  nqnq0a  7664  nqnq0m  7665  distrnq0  7669  nqprloc  7755  ltexprlemopl  7811  ltexprlemopu  7813  recexre  8748  nn1suc  9152  msqznn  9570  nn0ind  9584  fnn0ind  9586  ublbneg  9837  qreccl  9866  fzo1fzo0n0  10412  elfzom1elp1fzo  10437  fzo0end  10458  fzind2  10475  flqeqceilz  10570  nnsinds  10697  nn0sinds  10698  ser0f  10786  hashfacen  11090  iswrddm0  11127  swrdlsw  11240  pfxn0  11259  swrdswrdlem  11275  pfxccatin12lem3  11303  pfxccat3  11305  pfxccat3a  11309  swrdccat3blem  11310  redivap  11425  imdivap  11432  cvg1nlemres  11536  sqrt0  11555  summodclem3  11931  fsump1i  11984  prodf1  12093  cos1bnd  12310  odd2np1  12424  opoe  12446  omoe  12447  opeo  12448  omeo  12449  dfgcd2  12575  gcdmultiplez  12582  dvdssq  12592  algfx  12614  odzval  12804  mul4sq  12957  setsfun0  13108  rmodislmod  14355  isridl  14508  neipsm  14868  txbas  14972  elcncf1di  15293  plyco  15473  reeff1o  15487  sincosq1lem  15539  sincosq2sgn  15541  sincosq4sgn  15543  lgsne0  15757  2lgslem1  15810  mul2sq  15835  lpvtx  15920  umgrislfupgrenlem  15969  umgrislfupgrdom  15970  uspgr2wlkeq  16162  wlklenvclwlk  16170  bdbm1.3ii  16422