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  676  mtbii  678  orbi2d  795  pm3.11dc  963  prlem1  979  nfimd  1631  dral1  1776  cbvalv1  1797  cbvalh  1799  ax16i  1904  speiv  1908  a16g  1910  cbvalvw  1966  cbvexvw  1967  cleqh  2329  pm13.18  2481  rspcimdv  2908  rspcimedv  2909  rspcedv  2911  moi2  2984  moi  2986  eqrd  3242  abnexg  4537  ralxfrd  4553  ralxfr2d  4555  rexxfr2d  4556  elres  5041  2elresin  5434  f1ocnv  5587  tz6.12c  5659  fvun1  5702  dffo4  5785  isores3  5945  tposfo2  6419  issmo2  6441  iordsmo  6449  smoel2  6455  fiintim  7104  ismkvnex  7333  prarloclemarch  7616  genprndl  7719  genprndu  7720  ltpopr  7793  ltsopr  7794  recexprlem1ssl  7831  recexprlem1ssu  7832  aptiprlemu  7838  lttrsr  7960  aptap  8808  rerecapb  9001  nnmulcl  9142  nnnegz  9460  eluzdc  9817  negm  9822  iccid  10133  icoshft  10198  fzen  10251  elfz2nn0  10320  elfzom1p1elfzo  10432  flqeqceilz  10552  zmodidfzoimp  10588  swrd0g  11208  pfxccatin12lem2  11279  swrdccat  11283  swrdccat3blem  11287  caucvgre  11508  qdenre  11729  dvdsval2  12317  negdvdsb  12334  muldvds2  12344  dvdsabseq  12374  bezoutlemaz  12540  bezoutlembz  12541  rplpwr  12564  alginv  12585  algfx  12590  coprmgcdb  12626  divgcdcoprm0  12639  prmgt1  12670  oddprmgt2  12672  rpexp1i  12692  2sqpwodd  12714  qnumdencl  12725  phiprmpw  12760  prmdiveq  12774  prm23lt5  12802  pcmpt  12882  infpnlem1  12898  oddennn  12979  nninfdclemf1  13039  imasaddfnlemg  13363  aprcotr  14265  cnpnei  14909  bl2in  15093  addcncntoplem  15251  rescncf  15271  limcresi  15356  cnplimcim  15357  efltlemlt  15464  ioocosf1o  15544  2lgslem1a1  15781  clwwlkccatlem  16143  uzdcinzz  16245  bj-charfunbi  16257  bj-omssind  16381  bj-bdfindes  16395  bj-nntrans  16397  bj-nnelirr  16399  bj-omtrans  16402  setindis  16413  bdsetindis  16415  bj-inf2vnlem3  16418  bj-inf2vnlem4  16419  bj-findis  16425  bj-findes  16427