Theorem sylbir 133

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

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3imtr3i  198  3ori  1234  19.30dc  1561  nf4r  1604  cbvexh  1682  equveli  1686  sbequilem  1763  sb5rf  1777  nfsbxy  1863  nfsbxyt  1864  sbcomxyyz  1891  dvelimALT  1931  dvelimfv  1932  dvelimor  1939  mo2n  1973  mo23  1986  2exeu  2037  bm1.1  2070  necon1idc  2304  sbhypf  2662  vtocl2  2668  vtocl3  2669  reu6  2795  rmo2ilem  2917  uneqin  3239  abn0r  3296  inelcm  3331  vdif0im  3336  difrab0eqim  3337  r19.3rm  3357  r19.9rmv  3360  difprsn1  3559  intminss  3696  bm1.3ii  3935  intexabim  3963  copsex2g  4047  opelopabt  4063  eusv2nf  4252  reusv3i  4255  onintrab2im  4308  ordtri2orexmid  4312  setindel  4327  onsucuni2  4353  ordtri2or2exmid  4360  zfregfr  4362  tfi  4370  mosubopt  4471  eqrelrel  4507  xpiindim  4541  opeliunxp2  4544  opelrn  4637  issref  4781  xpmlem  4818  rnxpid  4831  ssxpbm  4832  relcoi2  4927  unixpm  4932  cnviinm  4938  iotanul  4961  funimaexglem  5062  fvelrnb  5315  fvmptssdm  5350  fnfvrnss  5421  fressnfv  5447  fconstfvm  5476  f1mpt  5511  ovprc  5641  fo1stresm  5889  fo2ndresm  5890  spc2ed  5955  reldmtpos  5972  tfrlem5  6033  tfrlem9  6038  tfri2  6085  frecfcllem  6123  frecsuclem  6125  fvmptmap  6394  ener  6448  domtr  6454  unen  6485  xpf1o  6512  mapen  6514  cardval3ex  6757  distrnqg  6890  nqnq0pi  6941  nqnq0a  6957  nqnq0m  6958  distrnq0  6962  nqprloc  7048  ltexprlemopl  7104  ltexprlemopu  7106  recexre  7996  nn1suc  8376  msqznn  8779  nn0ind  8793  fnn0ind  8795  ublbneg  9030  qreccl  9059  fzo1fzo0n0  9522  elfzom1elp1fzo  9541  fzo0end  9562  fzind2  9578  flqeqceilz  9653  nnsinds  9777  nn0sinds  9778  iser0f  9848  hashfacen  10137  redivap  10203  imdivap  10210  cvg1nlemres  10313  sqrt0  10332  isummolem3  10659  odd2np1  10748  opoe  10770  omoe  10771  opeo  10772  omeo  10773  dfgcd2  10878  gcdmultiplez  10885  dvdssq  10895  ialgfx  10909  bdbm1.3ii  11220