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  1289  19.30dc  1614  nf4r  1658  cbvexv1  1739  cbvexh  1742  equveli  1746  sbequilem  1825  sb5rf  1839  nfsbxy  1929  nfsbxyt  1930  sbcomxyyz  1959  dvelimALT  1997  dvelimfv  1998  dvelimor  2005  mo2n  2041  mo23  2054  2exeu  2105  bm1.1  2149  necon1idc  2387  sbhypf  2770  vtocl2  2776  vtocl3  2777  reu6  2910  rmo2ilem  3035  uneqin  3368  abn0r  3428  inelcm  3464  vdif0im  3469  difrab0eqim  3470  r19.3rm  3492  r19.9rmv  3495  difprsn1  3706  intminss  3843  disjnim  3967  bm1.3ii  4097  intexabim  4125  copsex2g  4218  opelopabt  4234  eusv2nf  4428  reusv3i  4431  onintrab2im  4489  ordtri2orexmid  4494  setindel  4509  onsucuni2  4535  ordtri2or2exmid  4542  zfregfr  4545  tfi  4553  mosubopt  4663  eqrelrel  4699  xpiindim  4735  opeliunxp2  4738  opelrn  4832  issref  4980  xpmlem  5018  rnxpid  5032  ssxpbm  5033  relcoi2  5128  unixpm  5133  cnviinm  5139  iotanul  5162  funimaexglem  5265  fvelrnb  5528  fvmptssdm  5564  fnfvrnss  5639  fressnfv  5666  fconstfvm  5697  f1mpt  5733  ovprc  5868  fo1stresm  6121  fo2ndresm  6122  spc2ed  6192  opeliunxp2f  6197  reldmtpos  6212  tfrlem5  6273  tfrlem9  6278  tfri2  6325  frecfcllem  6363  frecsuclem  6365  fvmptmap  6642  ixpiinm  6681  ixp0  6688  mptelixpg  6691  ener  6736  domtr  6742  unen  6773  xpf1o  6801  mapen  6803  ss1o0el1o  6869  cardval3ex  7132  distrnqg  7319  nqnq0pi  7370  nqnq0a  7386  nqnq0m  7387  distrnq0  7391  nqprloc  7477  ltexprlemopl  7533  ltexprlemopu  7535  recexre  8467  nn1suc  8867  msqznn  9282  nn0ind  9296  fnn0ind  9298  ublbneg  9542  qreccl  9571  fzo1fzo0n0  10108  elfzom1elp1fzo  10127  fzo0end  10148  fzind2  10164  flqeqceilz  10243  nnsinds  10368  nn0sinds  10369  ser0f  10440  hashfacen  10735  redivap  10802  imdivap  10809  cvg1nlemres  10913  sqrt0  10932  summodclem3  11307  fsump1i  11360  prodf1  11469  cos1bnd  11686  odd2np1  11795  opoe  11817  omoe  11818  opeo  11819  omeo  11820  dfgcd2  11932  gcdmultiplez  11939  dvdssq  11949  algfx  11963  odzval  12150  setsfun0  12367  neipsm  12695  txbas  12799  elcncf1di  13107  reeff1o  13235  sincosq1lem  13287  sincosq2sgn  13289  sincosq4sgn  13291  bdbm1.3ii  13608