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  1341  19.30dc  1680  nf4r  1723  cbvexv1  1805  cbvexh  1808  equveli  1812  sbequilem  1891  sb5rf  1905  nfsbxy  2002  nfsbxyt  2003  sbcomxyyz  2032  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  mo2n  2114  mo23  2128  2exeu  2179  bm1.1  2223  necon1idc  2473  sbhypf  2872  vtocl2  2878  vtocl3  2879  reu6  3015  rmo2ilem  3142  rabssrabd  3335  uneqin  3482  abn0r  3546  inelcm  3584  vdif0im  3589  difrab0eqim  3590  r19.3rm  3613  r19.9rmv  3616  difprsn1  3849  intminss  3990  disjnim  4115  bm1.3ii  4249  intexabim  4283  copsex2g  4381  opelopabt  4399  eusv2nf  4597  reusv3i  4600  onintrab2im  4660  ordtri2orexmid  4665  setindel  4680  onsucuni2  4706  ordtri2or2exmid  4713  zfregfr  4716  tfi  4724  mosubopt  4835  eqrelrel  4871  xpiindim  4912  opeliunxp2  4915  opelrn  5011  issref  5165  xpmlem  5203  rnxpid  5217  ssxpbm  5218  relcoi2  5313  unixpm  5318  cnviinm  5324  iotanul  5348  iotaexab  5351  funimaexglem  5459  fvelrnb  5744  fvmptssdm  5784  fnfvrnss  5859  fressnfv  5893  fconstfvm  5924  f1mpt  5967  ovprc  6111  fvmpopr2d  6215  fo1stresm  6385  fo2ndresm  6386  spc2ed  6459  opeliunxp2f  6499  reldmtpos  6514  tfrlem5  6575  tfrlem9  6580  tfri2  6627  frecfcllem  6665  frecsuclem  6667  fvmptmap  6956  ixpiinm  6996  ixp0  7003  mptelixpg  7006  ener  7056  domtr  7062  unen  7095  xpf1o  7134  mapen  7136  ss1o0el1o  7210  cardval3ex  7520  pr2cv2  7532  distrnqg  7744  nqnq0pi  7795  nqnq0a  7811  nqnq0m  7812  distrnq0  7816  nqprloc  7902  ltexprlemopl  7958  ltexprlemopu  7960  recexre  8896  nn1suc  9302  msqznn  9725  nn0ind  9739  fnn0ind  9741  ublbneg  9992  qreccl  10021  fzo1fzo0n0  10573  elfzom1elp1fzo  10598  fzo0end  10619  fzind2  10636  flqeqceilz  10733  nnsinds  10860  nn0sinds  10861  ser0f  10949  hashfacen  11262  iswrddm0  11306  swrdlsw  11419  pfxn0  11438  swrdswrdlem  11454  pfxccatin12lem3  11482  pfxccat3  11484  pfxccat3a  11488  swrdccat3blem  11489  redivap  11617  imdivap  11624  cvg1nlemres  11729  sqrt0  11748  summodclem3  12125  fsump1i  12178  prodf1  12287  cos1bnd  12504  odd2np1  12618  opoe  12640  omoe  12641  opeo  12642  omeo  12643  dfgcd2  12769  gcdmultiplez  12776  dvdssq  12786  algfx  12808  odzval  12998  mul4sq  13151  ballotfilemsdom  13233  ballotfilemth  13259  setsfun0  13366  rmodislmod  14660  isridl  14813  neipsm  15178  txbas  15282  elcncf1di  15603  plyco  15783  reeff1o  15797  sincosq1lem  15849  sincosq2sgn  15851  sincosq4sgn  15853  lgsne0  16071  2lgslem1  16124  mul2sq  16149  lpvtx  16234  umgrislfupgrenlem  16285  umgrislfupgrdom  16286  uspgr2wlkeq  16520  wlklenvclwlk  16528  bdbm1.3ii  16831