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-1 5  ax-2 6  ax-mp 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  1246  19.30dc  1574  nf4r  1617  cbvexh  1696  equveli  1700  sbequilem  1777  sb5rf  1791  nfsbxy  1878  nfsbxyt  1879  sbcomxyyz  1906  dvelimALT  1946  dvelimfv  1947  dvelimor  1954  mo2n  1988  mo23  2001  2exeu  2052  bm1.1  2085  necon1idc  2320  sbhypf  2690  vtocl2  2696  vtocl3  2697  reu6  2826  rmo2ilem  2950  uneqin  3274  abn0r  3334  inelcm  3370  vdif0im  3375  difrab0eqim  3376  r19.3rm  3398  r19.9rmv  3401  difprsn1  3606  intminss  3743  disjnim  3866  bm1.3ii  3989  intexabim  4017  copsex2g  4106  opelopabt  4122  eusv2nf  4315  reusv3i  4318  onintrab2im  4372  ordtri2orexmid  4376  setindel  4391  onsucuni2  4417  ordtri2or2exmid  4424  zfregfr  4426  tfi  4434  mosubopt  4542  eqrelrel  4578  xpiindim  4614  opeliunxp2  4617  opelrn  4711  issref  4857  xpmlem  4895  rnxpid  4909  ssxpbm  4910  relcoi2  5005  unixpm  5010  cnviinm  5016  iotanul  5039  funimaexglem  5142  fvelrnb  5401  fvmptssdm  5437  fnfvrnss  5512  fressnfv  5539  fconstfvm  5570  f1mpt  5604  ovprc  5738  fo1stresm  5990  fo2ndresm  5991  spc2ed  6060  opeliunxp2f  6065  reldmtpos  6080  tfrlem5  6141  tfrlem9  6146  tfri2  6193  frecfcllem  6231  frecsuclem  6233  fvmptmap  6509  ixpiinm  6548  ixp0  6555  mptelixpg  6558  ener  6603  domtr  6609  unen  6640  xpf1o  6667  mapen  6669  cardval3ex  6952  distrnqg  7096  nqnq0pi  7147  nqnq0a  7163  nqnq0m  7164  distrnq0  7168  nqprloc  7254  ltexprlemopl  7310  ltexprlemopu  7312  recexre  8206  nn1suc  8597  msqznn  9003  nn0ind  9017  fnn0ind  9019  ublbneg  9255  qreccl  9284  fzo1fzo0n0  9801  elfzom1elp1fzo  9820  fzo0end  9841  fzind2  9857  flqeqceilz  9932  nnsinds  10057  nn0sinds  10058  ser0f  10129  hashfacen  10420  redivap  10487  imdivap  10494  cvg1nlemres  10597  sqrt0  10616  summodclem3  10988  fsump1i  11041  cos1bnd  11264  odd2np1  11365  opoe  11387  omoe  11388  opeo  11389  omeo  11390  dfgcd2  11495  gcdmultiplez  11502  dvdssq  11512  algfx  11526  setsfun0  11777  neipsm  12105  txbas  12208  elcncf1di  12479  bdbm1.3ii  12670