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  2850  vtocl2  2856  vtocl3  2857  reu6  2992  rmo2ilem  3119  uneqin  3455  abn0r  3516  inelcm  3552  vdif0im  3557  difrab0eqim  3558  r19.3rm  3580  r19.9rmv  3583  difprsn1  3806  intminss  3947  disjnim  4072  bm1.3ii  4204  intexabim  4235  copsex2g  4331  opelopabt  4349  eusv2nf  4546  reusv3i  4549  onintrab2im  4609  ordtri2orexmid  4614  setindel  4629  onsucuni2  4655  ordtri2or2exmid  4662  zfregfr  4665  tfi  4673  mosubopt  4783  eqrelrel  4819  xpiindim  4858  opeliunxp2  4861  opelrn  4957  issref  5110  xpmlem  5148  rnxpid  5162  ssxpbm  5163  relcoi2  5258  unixpm  5263  cnviinm  5269  iotanul  5293  iotaexab  5296  funimaexglem  5403  fvelrnb  5680  fvmptssdm  5718  fnfvrnss  5794  fressnfv  5825  fconstfvm  5856  f1mpt  5894  ovprc  6036  fvmpopr2d  6140  fo1stresm  6305  fo2ndresm  6306  spc2ed  6377  opeliunxp2f  6382  reldmtpos  6397  tfrlem5  6458  tfrlem9  6463  tfri2  6510  frecfcllem  6548  frecsuclem  6550  fvmptmap  6830  ixpiinm  6869  ixp0  6876  mptelixpg  6879  ener  6929  domtr  6935  unen  6967  xpf1o  7001  mapen  7003  ss1o0el1o  7071  cardval3ex  7353  pr2cv2  7365  distrnqg  7570  nqnq0pi  7621  nqnq0a  7637  nqnq0m  7638  distrnq0  7642  nqprloc  7728  ltexprlemopl  7784  ltexprlemopu  7786  recexre  8721  nn1suc  9125  msqznn  9543  nn0ind  9557  fnn0ind  9559  ublbneg  9804  qreccl  9833  fzo1fzo0n0  10379  elfzom1elp1fzo  10403  fzo0end  10424  fzind2  10440  flqeqceilz  10535  nnsinds  10662  nn0sinds  10663  ser0f  10751  hashfacen  11053  iswrddm0  11090  swrdlsw  11196  pfxn0  11215  swrdswrdlem  11231  pfxccatin12lem3  11259  pfxccat3  11261  pfxccat3a  11265  swrdccat3blem  11266  redivap  11380  imdivap  11387  cvg1nlemres  11491  sqrt0  11510  summodclem3  11886  fsump1i  11939  prodf1  12048  cos1bnd  12265  odd2np1  12379  opoe  12401  omoe  12402  opeo  12403  omeo  12404  dfgcd2  12530  gcdmultiplez  12537  dvdssq  12547  algfx  12569  odzval  12759  mul4sq  12912  setsfun0  13063  rmodislmod  14309  isridl  14462  neipsm  14822  txbas  14926  elcncf1di  15247  plyco  15427  reeff1o  15441  sincosq1lem  15493  sincosq2sgn  15495  sincosq4sgn  15497  lgsne0  15711  2lgslem1  15764  mul2sq  15789  lpvtx  15873  umgrislfupgrenlem  15922  umgrislfupgrdom  15923  bdbm1.3ii  16212