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 ⊢ (𝜑 → (𝜒 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimtrrdi  164  mpbird  167  sylibrd  169  sylbird  170  imbi1d  231  biimpar  297  mtbid  683  mtbii  685  orbi2d  802  pm3.11dc  970  prlem1  986  nfimd  1638  dral1  1783  cbvalv1  1804  cbvalh  1806  ax16i  1911  speiv  1915  a16g  1917  cbvalvw  1975  cbvexvw  1976  cleqh  2338  pm13.18  2501  rspcimdv  2930  rspcimedv  2931  rspcedv  2933  moi2  3007  moi  3009  eqrd  3266  ifeqeqxdc  3687  rabsnifsb  3777  abnexg  4594  ralxfrd  4610  ralxfr2d  4612  rexxfr2d  4613  elres  5101  2elresin  5497  f1ocnv  5655  tz6.12c  5728  fvun1  5772  dffo4  5859  isores3  6024  fvdifsuppst  6488  tposfo2  6543  issmo2  6565  iordsmo  6573  smoel2  6579  fiintim  7244  ismkvnex  7501  prarloclemarch  7791  genprndl  7894  genprndu  7895  ltpopr  7968  ltsopr  7969  recexprlem1ssl  8006  recexprlem1ssu  8007  aptiprlemu  8013  lttrsr  8135  aptap  8986  rerecapb  9181  nnmulcl  9334  nnnegz  9656  eluzdc  10025  negm  10030  iccid  10343  icoshft  10408  fzen  10463  elfz2nn0  10535  elfzom1p1elfzo  10648  flqeqceilz  10775  zmodidfzoimp  10811  swrd0g  11453  pfxccatin12lem2  11524  swrdccat  11528  swrdccat3blem  11532  caucvgre  11768  qdenre  11990  dvdsval2  12581  negdvdsb  12598  muldvds2  12608  dvdsabseq  12638  bezoutlemaz  12804  bezoutlembz  12805  rplpwr  12828  alginv  12849  algfx  12854  coprmgcdb  12890  divgcdcoprm0  12903  prmgt1  12935  oddprmgt2  12937  rpexp1i  12957  2sqpwodd  12980  qnumdencl  12991  phiprmpw  13028  prmdiveq  13042  prm23lt5  13070  pcmpt  13150  infpnlem1  13166  oddennn  13340  nninfdclemf1  13400  imasaddfnlemg  13693  aprcotr  14705  cnpnei  15462  bl2in  15646  addcncntoplem  15804  rescncf  15824  limcresi  15909  cnplimcim  15910  efltlemlt  16017  ioocosf1o  16099  bposlem1  16328  bposlem5  16332  2lgslem1a1  16427  clwwlkccatlem  16863  clwwlknonex2lem2  16901  uzdcinzz  17048  bj-charfunbi  17059  bj-omssind  17183  bj-bdfindes  17197  bj-nntrans  17199  bj-nnelirr  17201  bj-omtrans  17204  setindis  17215  bdsetindis  17217  bj-inf2vnlem3  17220  bj-inf2vnlem4  17221  bj-findis  17227  bj-findes  17229