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  5609  fvmptssdm  5647  fnfvrnss  5723  fressnfv  5750  fconstfvm  5781  f1mpt  5819  ovprc  5959  fvmpopr2d  6061  fo1stresm  6221  fo2ndresm  6222  spc2ed  6293  opeliunxp2f  6298  reldmtpos  6313  tfrlem5  6374  tfrlem9  6379  tfri2  6426  frecfcllem  6464  frecsuclem  6466  fvmptmap  6746  ixpiinm  6785  ixp0  6792  mptelixpg  6795  ener  6840  domtr  6846  unen  6877  xpf1o  6907  mapen  6909  ss1o0el1o  6976  cardval3ex  7254  distrnqg  7457  nqnq0pi  7508  nqnq0a  7524  nqnq0m  7525  distrnq0  7529  nqprloc  7615  ltexprlemopl  7671  ltexprlemopu  7673  recexre  8608  nn1suc  9012  msqznn  9429  nn0ind  9443  fnn0ind  9445  ublbneg  9690  qreccl  9719  fzo1fzo0n0  10262  elfzom1elp1fzo  10281  fzo0end  10302  fzind2  10318  flqeqceilz  10413  nnsinds  10540  nn0sinds  10541  ser0f  10629  hashfacen  10931  iswrddm0  10962  redivap  11042  imdivap  11049  cvg1nlemres  11153  sqrt0  11172  summodclem3  11548  fsump1i  11601  prodf1  11710  cos1bnd  11927  odd2np1  12041  opoe  12063  omoe  12064  opeo  12065  omeo  12066  dfgcd2  12192  gcdmultiplez  12199  dvdssq  12209  algfx  12231  odzval  12421  mul4sq  12574  setsfun0  12725  rmodislmod  13933  isridl  14086  neipsm  14416  txbas  14520  elcncf1di  14841  plyco  15021  reeff1o  15035  sincosq1lem  15087  sincosq2sgn  15089  sincosq4sgn  15091  lgsne0  15305  2lgslem1  15358  mul2sq  15383  bdbm1.3ii  15563