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  1337  19.30dc  1676  nf4r  1719  cbvexv1  1801  cbvexh  1804  equveli  1808  sbequilem  1887  sb5rf  1901  nfsbxy  1996  nfsbxyt  1997  sbcomxyyz  2026  dvelimALT  2064  dvelimfv  2065  dvelimor  2072  mo2n  2108  mo23  2122  2exeu  2173  bm1.1  2217  necon1idc  2465  sbhypf  2864  vtocl2  2870  vtocl3  2871  reu6  3006  rmo2ilem  3133  rabssrabd  3325  uneqin  3472  abn0r  3533  inelcm  3569  vdif0im  3574  difrab0eqim  3575  r19.3rm  3598  r19.9rmv  3601  difprsn1  3833  intminss  3974  disjnim  4099  bm1.3ii  4231  intexabim  4264  copsex2g  4362  opelopabt  4380  eusv2nf  4577  reusv3i  4580  onintrab2im  4640  ordtri2orexmid  4645  setindel  4660  onsucuni2  4686  ordtri2or2exmid  4693  zfregfr  4696  tfi  4704  mosubopt  4815  eqrelrel  4851  xpiindim  4892  opeliunxp2  4895  opelrn  4991  issref  5145  xpmlem  5183  rnxpid  5197  ssxpbm  5198  relcoi2  5293  unixpm  5298  cnviinm  5304  iotanul  5328  iotaexab  5331  funimaexglem  5439  fvelrnb  5724  fvmptssdm  5762  fnfvrnss  5837  fressnfv  5871  fconstfvm  5902  f1mpt  5944  ovprc  6086  fvmpopr2d  6190  fo1stresm  6355  fo2ndresm  6356  spc2ed  6429  opeliunxp2f  6469  reldmtpos  6484  tfrlem5  6545  tfrlem9  6550  tfri2  6597  frecfcllem  6635  frecsuclem  6637  fvmptmap  6919  ixpiinm  6959  ixp0  6966  mptelixpg  6969  ener  7019  domtr  7025  unen  7058  xpf1o  7097  mapen  7099  ss1o0el1o  7173  cardval3ex  7481  pr2cv2  7493  distrnqg  7702  nqnq0pi  7753  nqnq0a  7769  nqnq0m  7770  distrnq0  7774  nqprloc  7860  ltexprlemopl  7916  ltexprlemopu  7918  recexre  8852  nn1suc  9256  msqznn  9678  nn0ind  9692  fnn0ind  9694  ublbneg  9945  qreccl  9974  fzo1fzo0n0  10522  elfzom1elp1fzo  10547  fzo0end  10568  fzind2  10585  flqeqceilz  10680  nnsinds  10807  nn0sinds  10808  ser0f  10896  hashfacen  11208  iswrddm0  11248  swrdlsw  11361  pfxn0  11380  swrdswrdlem  11396  pfxccatin12lem3  11424  pfxccat3  11426  pfxccat3a  11430  swrdccat3blem  11431  redivap  11559  imdivap  11566  cvg1nlemres  11670  sqrt0  11689  summodclem3  12066  fsump1i  12119  prodf1  12228  cos1bnd  12445  odd2np1  12559  opoe  12581  omoe  12582  opeo  12583  omeo  12584  dfgcd2  12710  gcdmultiplez  12717  dvdssq  12727  algfx  12749  odzval  12939  mul4sq  13092  setsfun0  13248  rmodislmod  14499  isridl  14652  neipsm  15019  txbas  15123  elcncf1di  15444  plyco  15624  reeff1o  15638  sincosq1lem  15690  sincosq2sgn  15692  sincosq4sgn  15694  lgsne0  15911  2lgslem1  15964  mul2sq  15989  lpvtx  16074  umgrislfupgrenlem  16125  umgrislfupgrdom  16126  uspgr2wlkeq  16360  wlklenvclwlk  16368  bdbm1.3ii  16661