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  1311  19.30dc  1641  nf4r  1685  cbvexv1  1766  cbvexh  1769  equveli  1773  sbequilem  1852  sb5rf  1866  nfsbxy  1961  nfsbxyt  1962  sbcomxyyz  1991  dvelimALT  2029  dvelimfv  2030  dvelimor  2037  mo2n  2073  mo23  2086  2exeu  2137  bm1.1  2181  necon1idc  2420  sbhypf  2813  vtocl2  2819  vtocl3  2820  reu6  2953  rmo2ilem  3079  uneqin  3415  abn0r  3476  inelcm  3512  vdif0im  3517  difrab0eqim  3518  r19.3rm  3540  r19.9rmv  3543  difprsn1  3762  intminss  3900  disjnim  4025  bm1.3ii  4155  intexabim  4186  copsex2g  4280  opelopabt  4297  eusv2nf  4492  reusv3i  4495  onintrab2im  4555  ordtri2orexmid  4560  setindel  4575  onsucuni2  4601  ordtri2or2exmid  4608  zfregfr  4611  tfi  4619  mosubopt  4729  eqrelrel  4765  xpiindim  4804  opeliunxp2  4807  opelrn  4901  issref  5053  xpmlem  5091  rnxpid  5105  ssxpbm  5106  relcoi2  5201  unixpm  5206  cnviinm  5212  iotanul  5235  iotaexab  5238  funimaexglem  5342  fvelrnb  5611  fvmptssdm  5649  fnfvrnss  5725  fressnfv  5752  fconstfvm  5783  f1mpt  5821  ovprc  5961  fvmpopr2d  6063  fo1stresm  6228  fo2ndresm  6229  spc2ed  6300  opeliunxp2f  6305  reldmtpos  6320  tfrlem5  6381  tfrlem9  6386  tfri2  6433  frecfcllem  6471  frecsuclem  6473  fvmptmap  6753  ixpiinm  6792  ixp0  6799  mptelixpg  6802  ener  6847  domtr  6853  unen  6884  xpf1o  6914  mapen  6916  ss1o0el1o  6983  cardval3ex  7263  distrnqg  7471  nqnq0pi  7522  nqnq0a  7538  nqnq0m  7539  distrnq0  7543  nqprloc  7629  ltexprlemopl  7685  ltexprlemopu  7687  recexre  8622  nn1suc  9026  msqznn  9443  nn0ind  9457  fnn0ind  9459  ublbneg  9704  qreccl  9733  fzo1fzo0n0  10276  elfzom1elp1fzo  10295  fzo0end  10316  fzind2  10332  flqeqceilz  10427  nnsinds  10554  nn0sinds  10555  ser0f  10643  hashfacen  10945  iswrddm0  10976  redivap  11056  imdivap  11063  cvg1nlemres  11167  sqrt0  11186  summodclem3  11562  fsump1i  11615  prodf1  11724  cos1bnd  11941  odd2np1  12055  opoe  12077  omoe  12078  opeo  12079  omeo  12080  dfgcd2  12206  gcdmultiplez  12213  dvdssq  12223  algfx  12245  odzval  12435  mul4sq  12588  setsfun0  12739  rmodislmod  13983  isridl  14136  neipsm  14474  txbas  14578  elcncf1di  14899  plyco  15079  reeff1o  15093  sincosq1lem  15145  sincosq2sgn  15147  sincosq4sgn  15149  lgsne0  15363  2lgslem1  15416  mul2sq  15441  bdbm1.3ii  15621