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  1337  19.30dc  1676  nf4r  1719  cbvexv1  1800  cbvexh  1803  equveli  1807  sbequilem  1886  sb5rf  1900  nfsbxy  1995  nfsbxyt  1996  sbcomxyyz  2025  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  mo2n  2107  mo23  2121  2exeu  2172  bm1.1  2216  necon1idc  2456  sbhypf  2854  vtocl2  2860  vtocl3  2861  reu6  2996  rmo2ilem  3123  rabssrabd  3315  uneqin  3460  abn0r  3521  inelcm  3557  vdif0im  3562  difrab0eqim  3563  r19.3rm  3585  r19.9rmv  3588  difprsn1  3817  intminss  3958  disjnim  4083  bm1.3ii  4215  intexabim  4247  copsex2g  4344  opelopabt  4362  eusv2nf  4559  reusv3i  4562  onintrab2im  4622  ordtri2orexmid  4627  setindel  4642  onsucuni2  4668  ordtri2or2exmid  4675  zfregfr  4678  tfi  4686  mosubopt  4797  eqrelrel  4833  xpiindim  4873  opeliunxp2  4876  opelrn  4972  issref  5126  xpmlem  5164  rnxpid  5178  ssxpbm  5179  relcoi2  5274  unixpm  5279  cnviinm  5285  iotanul  5309  iotaexab  5312  funimaexglem  5420  fvelrnb  5702  fvmptssdm  5740  fnfvrnss  5815  fressnfv  5849  fconstfvm  5880  f1mpt  5922  ovprc  6064  fvmpopr2d  6168  fo1stresm  6333  fo2ndresm  6334  spc2ed  6407  opeliunxp2f  6447  reldmtpos  6462  tfrlem5  6523  tfrlem9  6528  tfri2  6575  frecfcllem  6613  frecsuclem  6615  fvmptmap  6897  ixpiinm  6936  ixp0  6943  mptelixpg  6946  ener  6996  domtr  7002  unen  7034  xpf1o  7073  mapen  7075  ss1o0el1o  7148  cardval3ex  7432  pr2cv2  7444  distrnqg  7650  nqnq0pi  7701  nqnq0a  7717  nqnq0m  7718  distrnq0  7722  nqprloc  7808  ltexprlemopl  7864  ltexprlemopu  7866  recexre  8800  nn1suc  9204  msqznn  9624  nn0ind  9638  fnn0ind  9640  ublbneg  9891  qreccl  9920  fzo1fzo0n0  10468  elfzom1elp1fzo  10493  fzo0end  10514  fzind2  10531  flqeqceilz  10626  nnsinds  10753  nn0sinds  10754  ser0f  10842  hashfacen  11146  iswrddm0  11186  swrdlsw  11299  pfxn0  11318  swrdswrdlem  11334  pfxccatin12lem3  11362  pfxccat3  11364  pfxccat3a  11368  swrdccat3blem  11369  redivap  11497  imdivap  11504  cvg1nlemres  11608  sqrt0  11627  summodclem3  12004  fsump1i  12057  prodf1  12166  cos1bnd  12383  odd2np1  12497  opoe  12519  omoe  12520  opeo  12521  omeo  12522  dfgcd2  12648  gcdmultiplez  12655  dvdssq  12665  algfx  12687  odzval  12877  mul4sq  13030  setsfun0  13181  rmodislmod  14430  isridl  14583  neipsm  14948  txbas  15052  elcncf1di  15373  plyco  15553  reeff1o  15567  sincosq1lem  15619  sincosq2sgn  15621  sincosq4sgn  15623  lgsne0  15840  2lgslem1  15893  mul2sq  15918  lpvtx  16003  umgrislfupgrenlem  16054  umgrislfupgrdom  16055  uspgr2wlkeq  16289  wlklenvclwlk  16297  bdbm1.3ii  16590