Theorem biimprd 158

Description: Deduce a converse implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)

Hypothesis

Ref	Expression
biimprd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimprd	⊢ (𝜑 → (𝜒 → 𝜓))

Proof of Theorem biimprd

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜒 → 𝜒)
2		biimprd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	imbitrrid 156	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:  biimtrrdi  164  mpbird  167  sylibrd  169  sylbird  170  imbi1d  231  biimpar  297  mtbid  674  mtbii  676  orbi2d  792  pm3.11dc  960  prlem1  976  nfimd  1608  dral1  1753  cbvalv1  1774  cbvalh  1776  ax16i  1881  speiv  1885  a16g  1887  cbvalvw  1943  cbvexvw  1944  cleqh  2305  pm13.18  2457  rspcimdv  2878  rspcimedv  2879  rspcedv  2881  moi2  2954  moi  2956  eqrd  3211  abnexg  4494  ralxfrd  4510  ralxfr2d  4512  rexxfr2d  4513  elres  4996  2elresin  5388  f1ocnv  5537  tz6.12c  5608  fvun1  5647  dffo4  5730  isores3  5886  tposfo2  6355  issmo2  6377  iordsmo  6385  smoel2  6391  fiintim  7030  ismkvnex  7259  prarloclemarch  7533  genprndl  7636  genprndu  7637  ltpopr  7710  ltsopr  7711  recexprlem1ssl  7748  recexprlem1ssu  7749  aptiprlemu  7755  lttrsr  7877  aptap  8725  rerecapb  8918  nnmulcl  9059  nnnegz  9377  eluzdc  9733  negm  9738  iccid  10049  icoshft  10114  fzen  10167  elfz2nn0  10236  elfzom1p1elfzo  10345  flqeqceilz  10465  zmodidfzoimp  10501  swrd0g  11116  caucvgre  11325  qdenre  11546  dvdsval2  12134  negdvdsb  12151  muldvds2  12161  dvdsabseq  12191  bezoutlemaz  12357  bezoutlembz  12358  rplpwr  12381  alginv  12402  algfx  12407  coprmgcdb  12443  divgcdcoprm0  12456  prmgt1  12487  oddprmgt2  12489  rpexp1i  12509  2sqpwodd  12531  qnumdencl  12542  phiprmpw  12577  prmdiveq  12591  prm23lt5  12619  pcmpt  12699  infpnlem1  12715  oddennn  12796  nninfdclemf1  12856  imasaddfnlemg  13179  aprcotr  14080  cnpnei  14724  bl2in  14908  addcncntoplem  15066  rescncf  15086  limcresi  15171  cnplimcim  15172  efltlemlt  15279  ioocosf1o  15359  2lgslem1a1  15596  uzdcinzz  15771  bj-charfunbi  15784  bj-omssind  15908  bj-bdfindes  15922  bj-nntrans  15924  bj-nnelirr  15926  bj-omtrans  15929  setindis  15940  bdsetindis  15942  bj-inf2vnlem3  15945  bj-inf2vnlem4  15946  bj-findis  15952  bj-findes  15954