Theorem sylbir 134

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 132	. 2 ⊢ (𝜑 → 𝜓)
3		sylbir.2	. 2 ⊢ (𝜓 → 𝜒)
4	2, 3	syl 14	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr3i  199  3ori  1290  19.30dc  1615  nf4r  1659  cbvexv1  1740  cbvexh  1743  equveli  1747  sbequilem  1826  sb5rf  1840  nfsbxy  1930  nfsbxyt  1931  sbcomxyyz  1960  dvelimALT  1998  dvelimfv  1999  dvelimor  2006  mo2n  2042  mo23  2055  2exeu  2106  bm1.1  2150  necon1idc  2389  sbhypf  2775  vtocl2  2781  vtocl3  2782  reu6  2915  rmo2ilem  3040  uneqin  3373  abn0r  3433  inelcm  3469  vdif0im  3474  difrab0eqim  3475  r19.3rm  3497  r19.9rmv  3500  difprsn1  3712  intminss  3849  disjnim  3973  bm1.3ii  4103  intexabim  4131  copsex2g  4224  opelopabt  4240  eusv2nf  4434  reusv3i  4437  onintrab2im  4495  ordtri2orexmid  4500  setindel  4515  onsucuni2  4541  ordtri2or2exmid  4548  zfregfr  4551  tfi  4559  mosubopt  4669  eqrelrel  4705  xpiindim  4741  opeliunxp2  4744  opelrn  4838  issref  4986  xpmlem  5024  rnxpid  5038  ssxpbm  5039  relcoi2  5134  unixpm  5139  cnviinm  5145  iotanul  5168  funimaexglem  5271  fvelrnb  5534  fvmptssdm  5570  fnfvrnss  5645  fressnfv  5672  fconstfvm  5703  f1mpt  5739  ovprc  5877  fo1stresm  6129  fo2ndresm  6130  spc2ed  6201  opeliunxp2f  6206  reldmtpos  6221  tfrlem5  6282  tfrlem9  6287  tfri2  6334  frecfcllem  6372  frecsuclem  6374  fvmptmap  6651  ixpiinm  6690  ixp0  6697  mptelixpg  6700  ener  6745  domtr  6751  unen  6782  xpf1o  6810  mapen  6812  ss1o0el1o  6878  cardval3ex  7141  distrnqg  7328  nqnq0pi  7379  nqnq0a  7395  nqnq0m  7396  distrnq0  7400  nqprloc  7486  ltexprlemopl  7542  ltexprlemopu  7544  recexre  8476  nn1suc  8876  msqznn  9291  nn0ind  9305  fnn0ind  9307  ublbneg  9551  qreccl  9580  fzo1fzo0n0  10118  elfzom1elp1fzo  10137  fzo0end  10158  fzind2  10174  flqeqceilz  10253  nnsinds  10378  nn0sinds  10379  ser0f  10450  hashfacen  10749  redivap  10816  imdivap  10823  cvg1nlemres  10927  sqrt0  10946  summodclem3  11321  fsump1i  11374  prodf1  11483  cos1bnd  11700  odd2np1  11810  opoe  11832  omoe  11833  opeo  11834  omeo  11835  dfgcd2  11947  gcdmultiplez  11954  dvdssq  11964  algfx  11984  odzval  12173  mul4sq  12324  setsfun0  12430  neipsm  12794  txbas  12898  elcncf1di  13206  reeff1o  13334  sincosq1lem  13386  sincosq2sgn  13388  sincosq4sgn  13390  lgsne0  13579  mul2sq  13592  bdbm1.3ii  13773