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  1312  19.30dc  1649  nf4r  1693  cbvexv1  1774  cbvexh  1777  equveli  1781  sbequilem  1860  sb5rf  1874  nfsbxy  1969  nfsbxyt  1970  sbcomxyyz  1999  dvelimALT  2037  dvelimfv  2038  dvelimor  2045  mo2n  2081  mo23  2094  2exeu  2145  bm1.1  2189  necon1idc  2428  sbhypf  2821  vtocl2  2827  vtocl3  2828  reu6  2961  rmo2ilem  3087  uneqin  3423  abn0r  3484  inelcm  3520  vdif0im  3525  difrab0eqim  3526  r19.3rm  3548  r19.9rmv  3551  difprsn1  3771  intminss  3909  disjnim  4034  bm1.3ii  4164  intexabim  4195  copsex2g  4289  opelopabt  4307  eusv2nf  4502  reusv3i  4505  onintrab2im  4565  ordtri2orexmid  4570  setindel  4585  onsucuni2  4611  ordtri2or2exmid  4618  zfregfr  4621  tfi  4629  mosubopt  4739  eqrelrel  4775  xpiindim  4814  opeliunxp2  4817  opelrn  4911  issref  5064  xpmlem  5102  rnxpid  5116  ssxpbm  5117  relcoi2  5212  unixpm  5217  cnviinm  5223  iotanul  5246  iotaexab  5249  funimaexglem  5356  fvelrnb  5625  fvmptssdm  5663  fnfvrnss  5739  fressnfv  5770  fconstfvm  5801  f1mpt  5839  ovprc  5979  fvmpopr2d  6081  fo1stresm  6246  fo2ndresm  6247  spc2ed  6318  opeliunxp2f  6323  reldmtpos  6338  tfrlem5  6399  tfrlem9  6404  tfri2  6451  frecfcllem  6489  frecsuclem  6491  fvmptmap  6771  ixpiinm  6810  ixp0  6817  mptelixpg  6820  ener  6870  domtr  6876  unen  6907  xpf1o  6940  mapen  6942  ss1o0el1o  7009  cardval3ex  7291  distrnqg  7499  nqnq0pi  7550  nqnq0a  7566  nqnq0m  7567  distrnq0  7571  nqprloc  7657  ltexprlemopl  7713  ltexprlemopu  7715  recexre  8650  nn1suc  9054  msqznn  9472  nn0ind  9486  fnn0ind  9488  ublbneg  9733  qreccl  9762  fzo1fzo0n0  10305  elfzom1elp1fzo  10329  fzo0end  10350  fzind2  10366  flqeqceilz  10461  nnsinds  10588  nn0sinds  10589  ser0f  10677  hashfacen  10979  iswrddm0  11016  redivap  11127  imdivap  11134  cvg1nlemres  11238  sqrt0  11257  summodclem3  11633  fsump1i  11686  prodf1  11795  cos1bnd  12012  odd2np1  12126  opoe  12148  omoe  12149  opeo  12150  omeo  12151  dfgcd2  12277  gcdmultiplez  12284  dvdssq  12294  algfx  12316  odzval  12506  mul4sq  12659  setsfun0  12810  rmodislmod  14055  isridl  14208  neipsm  14568  txbas  14672  elcncf1di  14993  plyco  15173  reeff1o  15187  sincosq1lem  15239  sincosq2sgn  15241  sincosq4sgn  15243  lgsne0  15457  2lgslem1  15510  mul2sq  15535  bdbm1.3ii  15760