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  1311  19.30dc  1638  nf4r  1682  cbvexv1  1763  cbvexh  1766  equveli  1770  sbequilem  1849  sb5rf  1863  nfsbxy  1958  nfsbxyt  1959  sbcomxyyz  1988  dvelimALT  2026  dvelimfv  2027  dvelimor  2034  mo2n  2070  mo23  2083  2exeu  2134  bm1.1  2178  necon1idc  2417  sbhypf  2810  vtocl2  2816  vtocl3  2817  reu6  2950  rmo2ilem  3076  uneqin  3411  abn0r  3472  inelcm  3508  vdif0im  3513  difrab0eqim  3514  r19.3rm  3536  r19.9rmv  3539  difprsn1  3758  intminss  3896  disjnim  4021  bm1.3ii  4151  intexabim  4182  copsex2g  4276  opelopabt  4293  eusv2nf  4488  reusv3i  4491  onintrab2im  4551  ordtri2orexmid  4556  setindel  4571  onsucuni2  4597  ordtri2or2exmid  4604  zfregfr  4607  tfi  4615  mosubopt  4725  eqrelrel  4761  xpiindim  4800  opeliunxp2  4803  opelrn  4897  issref  5049  xpmlem  5087  rnxpid  5101  ssxpbm  5102  relcoi2  5197  unixpm  5202  cnviinm  5208  iotanul  5231  iotaexab  5234  funimaexglem  5338  fvelrnb  5605  fvmptssdm  5643  fnfvrnss  5719  fressnfv  5746  fconstfvm  5777  f1mpt  5815  ovprc  5954  fvmpopr2d  6056  fo1stresm  6216  fo2ndresm  6217  spc2ed  6288  opeliunxp2f  6293  reldmtpos  6308  tfrlem5  6369  tfrlem9  6374  tfri2  6421  frecfcllem  6459  frecsuclem  6461  fvmptmap  6741  ixpiinm  6780  ixp0  6787  mptelixpg  6790  ener  6835  domtr  6841  unen  6872  xpf1o  6902  mapen  6904  ss1o0el1o  6971  cardval3ex  7247  distrnqg  7449  nqnq0pi  7500  nqnq0a  7516  nqnq0m  7517  distrnq0  7521  nqprloc  7607  ltexprlemopl  7663  ltexprlemopu  7665  recexre  8599  nn1suc  9003  msqznn  9420  nn0ind  9434  fnn0ind  9436  ublbneg  9681  qreccl  9710  fzo1fzo0n0  10253  elfzom1elp1fzo  10272  fzo0end  10293  fzind2  10309  flqeqceilz  10392  nnsinds  10519  nn0sinds  10520  ser0f  10608  hashfacen  10910  iswrddm0  10941  redivap  11021  imdivap  11028  cvg1nlemres  11132  sqrt0  11151  summodclem3  11526  fsump1i  11579  prodf1  11688  cos1bnd  11905  odd2np1  12017  opoe  12039  omoe  12040  opeo  12041  omeo  12042  dfgcd2  12154  gcdmultiplez  12161  dvdssq  12171  algfx  12193  odzval  12382  mul4sq  12535  setsfun0  12657  rmodislmod  13850  isridl  14003  neipsm  14333  txbas  14437  elcncf1di  14758  plyco  14937  reeff1o  14949  sincosq1lem  15001  sincosq2sgn  15003  sincosq4sgn  15005  lgsne0  15195  2lgslem1  15248  mul2sq  15273  bdbm1.3ii  15453