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  1313  19.30dc  1651  nf4r  1695  cbvexv1  1776  cbvexh  1779  equveli  1783  sbequilem  1862  sb5rf  1876  nfsbxy  1971  nfsbxyt  1972  sbcomxyyz  2001  dvelimALT  2039  dvelimfv  2040  dvelimor  2047  mo2n  2083  mo23  2096  2exeu  2147  bm1.1  2191  necon1idc  2430  sbhypf  2824  vtocl2  2830  vtocl3  2831  reu6  2966  rmo2ilem  3092  uneqin  3428  abn0r  3489  inelcm  3525  vdif0im  3530  difrab0eqim  3531  r19.3rm  3553  r19.9rmv  3556  difprsn1  3778  intminss  3916  disjnim  4041  bm1.3ii  4173  intexabim  4204  copsex2g  4298  opelopabt  4316  eusv2nf  4511  reusv3i  4514  onintrab2im  4574  ordtri2orexmid  4579  setindel  4594  onsucuni2  4620  ordtri2or2exmid  4627  zfregfr  4630  tfi  4638  mosubopt  4748  eqrelrel  4784  xpiindim  4823  opeliunxp2  4826  opelrn  4921  issref  5074  xpmlem  5112  rnxpid  5126  ssxpbm  5127  relcoi2  5222  unixpm  5227  cnviinm  5233  iotanul  5256  iotaexab  5259  funimaexglem  5366  fvelrnb  5639  fvmptssdm  5677  fnfvrnss  5753  fressnfv  5784  fconstfvm  5815  f1mpt  5853  ovprc  5993  fvmpopr2d  6095  fo1stresm  6260  fo2ndresm  6261  spc2ed  6332  opeliunxp2f  6337  reldmtpos  6352  tfrlem5  6413  tfrlem9  6418  tfri2  6465  frecfcllem  6503  frecsuclem  6505  fvmptmap  6785  ixpiinm  6824  ixp0  6831  mptelixpg  6834  ener  6884  domtr  6890  unen  6922  xpf1o  6956  mapen  6958  ss1o0el1o  7025  cardval3ex  7307  distrnqg  7520  nqnq0pi  7571  nqnq0a  7587  nqnq0m  7588  distrnq0  7592  nqprloc  7678  ltexprlemopl  7734  ltexprlemopu  7736  recexre  8671  nn1suc  9075  msqznn  9493  nn0ind  9507  fnn0ind  9509  ublbneg  9754  qreccl  9783  fzo1fzo0n0  10329  elfzom1elp1fzo  10353  fzo0end  10374  fzind2  10390  flqeqceilz  10485  nnsinds  10612  nn0sinds  10613  ser0f  10701  hashfacen  11003  iswrddm0  11040  swrdlsw  11145  pfxn0  11164  swrdswrdlem  11180  redivap  11260  imdivap  11267  cvg1nlemres  11371  sqrt0  11390  summodclem3  11766  fsump1i  11819  prodf1  11928  cos1bnd  12145  odd2np1  12259  opoe  12281  omoe  12282  opeo  12283  omeo  12284  dfgcd2  12410  gcdmultiplez  12417  dvdssq  12427  algfx  12449  odzval  12639  mul4sq  12792  setsfun0  12943  rmodislmod  14188  isridl  14341  neipsm  14701  txbas  14805  elcncf1di  15126  plyco  15306  reeff1o  15320  sincosq1lem  15372  sincosq2sgn  15374  sincosq4sgn  15376  lgsne0  15590  2lgslem1  15643  mul2sq  15668  lpvtx  15750  bdbm1.3ii  15965