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  679  mtbii  681  orbi2d  798  pm3.11dc  966  prlem1  982  nfimd  1634  dral1  1779  cbvalv1  1800  cbvalh  1802  ax16i  1907  speiv  1911  a16g  1913  cbvalvw  1971  cbvexvw  1972  cleqh  2334  pm13.18  2495  rspcimdv  2924  rspcimedv  2925  rspcedv  2927  moi2  3001  moi  3003  eqrd  3260  ifeqeqxdc  3673  rabsnifsb  3762  abnexg  4572  ralxfrd  4588  ralxfr2d  4590  rexxfr2d  4591  elres  5079  2elresin  5474  f1ocnv  5632  tz6.12c  5705  fvun1  5748  dffo4  5830  isores3  5994  fvdifsuppst  6457  tposfo2  6511  issmo2  6533  iordsmo  6541  smoel2  6547  fiintim  7204  ismkvnex  7459  prarloclemarch  7749  genprndl  7852  genprndu  7853  ltpopr  7926  ltsopr  7927  recexprlem1ssl  7964  recexprlem1ssu  7965  aptiprlemu  7971  lttrsr  8093  aptap  8941  rerecapb  9134  nnmulcl  9275  nnnegz  9597  eluzdc  9960  negm  9965  iccid  10277  icoshft  10342  fzen  10397  elfz2nn0  10468  elfzom1p1elfzo  10581  flqeqceilz  10704  zmodidfzoimp  10740  swrd0g  11377  pfxccatin12lem2  11448  swrdccat  11452  swrdccat3blem  11456  caucvgre  11691  qdenre  11912  dvdsval2  12501  negdvdsb  12518  muldvds2  12528  dvdsabseq  12558  bezoutlemaz  12724  bezoutlembz  12725  rplpwr  12748  alginv  12769  algfx  12774  coprmgcdb  12810  divgcdcoprm0  12823  prmgt1  12854  oddprmgt2  12856  rpexp1i  12876  2sqpwodd  12898  qnumdencl  12909  phiprmpw  12944  prmdiveq  12958  prm23lt5  12986  pcmpt  13066  infpnlem1  13082  oddennn  13227  nninfdclemf1  13287  imasaddfnlemg  13578  aprcotr  14535  cnpnei  15210  bl2in  15394  addcncntoplem  15552  rescncf  15572  limcresi  15657  cnplimcim  15658  efltlemlt  15765  ioocosf1o  15845  2lgslem1a1  16085  clwwlkccatlem  16521  clwwlknonex2lem2  16559  uzdcinzz  16696  bj-charfunbi  16707  bj-omssind  16831  bj-bdfindes  16845  bj-nntrans  16847  bj-nnelirr  16849  bj-omtrans  16852  setindis  16863  bdsetindis  16865  bj-inf2vnlem3  16868  bj-inf2vnlem4  16869  bj-findis  16875  bj-findes  16877