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  1278  19.30dc  1606  nf4r  1649  cbvexh  1728  equveli  1732  sbequilem  1810  sb5rf  1824  nfsbxy  1915  nfsbxyt  1916  sbcomxyyz  1945  dvelimALT  1985  dvelimfv  1986  dvelimor  1993  mo2n  2027  mo23  2040  2exeu  2091  bm1.1  2124  necon1idc  2361  sbhypf  2735  vtocl2  2741  vtocl3  2742  reu6  2873  rmo2ilem  2998  uneqin  3327  abn0r  3387  inelcm  3423  vdif0im  3428  difrab0eqim  3429  r19.3rm  3451  r19.9rmv  3454  difprsn1  3659  intminss  3796  disjnim  3920  bm1.3ii  4049  intexabim  4077  copsex2g  4168  opelopabt  4184  eusv2nf  4377  reusv3i  4380  onintrab2im  4434  ordtri2orexmid  4438  setindel  4453  onsucuni2  4479  ordtri2or2exmid  4486  zfregfr  4488  tfi  4496  mosubopt  4604  eqrelrel  4640  xpiindim  4676  opeliunxp2  4679  opelrn  4773  issref  4921  xpmlem  4959  rnxpid  4973  ssxpbm  4974  relcoi2  5069  unixpm  5074  cnviinm  5080  iotanul  5103  funimaexglem  5206  fvelrnb  5469  fvmptssdm  5505  fnfvrnss  5580  fressnfv  5607  fconstfvm  5638  f1mpt  5672  ovprc  5806  fo1stresm  6059  fo2ndresm  6060  spc2ed  6130  opeliunxp2f  6135  reldmtpos  6150  tfrlem5  6211  tfrlem9  6216  tfri2  6263  frecfcllem  6301  frecsuclem  6303  fvmptmap  6579  ixpiinm  6618  ixp0  6625  mptelixpg  6628  ener  6673  domtr  6679  unen  6710  xpf1o  6738  mapen  6740  cardval3ex  7041  distrnqg  7195  nqnq0pi  7246  nqnq0a  7262  nqnq0m  7263  distrnq0  7267  nqprloc  7353  ltexprlemopl  7409  ltexprlemopu  7411  recexre  8340  nn1suc  8739  msqznn  9151  nn0ind  9165  fnn0ind  9167  ublbneg  9405  qreccl  9434  fzo1fzo0n0  9960  elfzom1elp1fzo  9979  fzo0end  10000  fzind2  10016  flqeqceilz  10091  nnsinds  10216  nn0sinds  10217  ser0f  10288  hashfacen  10579  redivap  10646  imdivap  10653  cvg1nlemres  10757  sqrt0  10776  summodclem3  11149  fsump1i  11202  prodf1  11311  cos1bnd  11466  odd2np1  11570  opoe  11592  omoe  11593  opeo  11594  omeo  11595  dfgcd2  11702  gcdmultiplez  11709  dvdssq  11719  algfx  11733  setsfun0  11995  neipsm  12323  txbas  12427  elcncf1di  12735  sincosq1lem  12906  sincosq2sgn  12908  sincosq4sgn  12910  bdbm1.3ii  13089