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  1954  nfsbxyt  1955  sbcomxyyz  1984  dvelimALT  2022  dvelimfv  2023  dvelimor  2030  mo2n  2066  mo23  2079  2exeu  2130  bm1.1  2174  necon1idc  2413  sbhypf  2801  vtocl2  2807  vtocl3  2808  reu6  2941  rmo2ilem  3067  uneqin  3401  abn0r  3462  inelcm  3498  vdif0im  3503  difrab0eqim  3504  r19.3rm  3526  r19.9rmv  3529  difprsn1  3746  intminss  3884  disjnim  4009  bm1.3ii  4139  intexabim  4170  copsex2g  4264  opelopabt  4280  eusv2nf  4474  reusv3i  4477  onintrab2im  4535  ordtri2orexmid  4540  setindel  4555  onsucuni2  4581  ordtri2or2exmid  4588  zfregfr  4591  tfi  4599  mosubopt  4709  eqrelrel  4745  xpiindim  4782  opeliunxp2  4785  opelrn  4879  issref  5029  xpmlem  5067  rnxpid  5081  ssxpbm  5082  relcoi2  5177  unixpm  5182  cnviinm  5188  iotanul  5211  iotaexab  5214  funimaexglem  5318  fvelrnb  5584  fvmptssdm  5621  fnfvrnss  5697  fressnfv  5724  fconstfvm  5755  f1mpt  5793  ovprc  5932  fo1stresm  6187  fo2ndresm  6188  spc2ed  6259  opeliunxp2f  6264  reldmtpos  6279  tfrlem5  6340  tfrlem9  6345  tfri2  6392  frecfcllem  6430  frecsuclem  6432  fvmptmap  6712  ixpiinm  6751  ixp0  6758  mptelixpg  6761  ener  6806  domtr  6812  unen  6843  xpf1o  6873  mapen  6875  ss1o0el1o  6942  cardval3ex  7215  distrnqg  7417  nqnq0pi  7468  nqnq0a  7484  nqnq0m  7485  distrnq0  7489  nqprloc  7575  ltexprlemopl  7631  ltexprlemopu  7633  recexre  8566  nn1suc  8969  msqznn  9384  nn0ind  9398  fnn0ind  9400  ublbneg  9645  qreccl  9674  fzo1fzo0n0  10215  elfzom1elp1fzo  10234  fzo0end  10255  fzind2  10271  flqeqceilz  10351  nnsinds  10476  nn0sinds  10477  ser0f  10549  hashfacen  10851  redivap  10918  imdivap  10925  cvg1nlemres  11029  sqrt0  11048  summodclem3  11423  fsump1i  11476  prodf1  11585  cos1bnd  11802  odd2np1  11913  opoe  11935  omoe  11936  opeo  11937  omeo  11938  dfgcd2  12050  gcdmultiplez  12057  dvdssq  12067  algfx  12087  odzval  12276  mul4sq  12429  setsfun0  12551  rmodislmod  13684  isridl  13836  neipsm  14131  txbas  14235  elcncf1di  14543  reeff1o  14671  sincosq1lem  14723  sincosq2sgn  14725  sincosq4sgn  14727  lgsne0  14917  mul2sq  14941  bdbm1.3ii  15121