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  673  mtbii  675  orbi2d  791  pm3.11dc  959  prlem1  975  nfimd  1599  dral1  1744  cbvalv1  1765  cbvalh  1767  ax16i  1872  speiv  1876  a16g  1878  cbvalvw  1934  cbvexvw  1935  cleqh  2296  pm13.18  2448  rspcimdv  2869  rspcimedv  2870  rspcedv  2872  moi2  2945  moi  2947  eqrd  3202  abnexg  4482  ralxfrd  4498  ralxfr2d  4500  rexxfr2d  4501  elres  4983  2elresin  5372  f1ocnv  5520  tz6.12c  5591  fvun1  5630  dffo4  5713  isores3  5865  tposfo2  6334  issmo2  6356  iordsmo  6364  smoel2  6370  fiintim  7001  ismkvnex  7230  prarloclemarch  7504  genprndl  7607  genprndu  7608  ltpopr  7681  ltsopr  7682  recexprlem1ssl  7719  recexprlem1ssu  7720  aptiprlemu  7726  lttrsr  7848  aptap  8696  rerecapb  8889  nnmulcl  9030  nnnegz  9348  eluzdc  9703  negm  9708  iccid  10019  icoshft  10084  fzen  10137  elfz2nn0  10206  elfzom1p1elfzo  10309  flqeqceilz  10429  zmodidfzoimp  10465  caucvgre  11165  qdenre  11386  dvdsval2  11974  negdvdsb  11991  muldvds2  12001  dvdsabseq  12031  bezoutlemaz  12197  bezoutlembz  12198  rplpwr  12221  alginv  12242  algfx  12247  coprmgcdb  12283  divgcdcoprm0  12296  prmgt1  12327  oddprmgt2  12329  rpexp1i  12349  2sqpwodd  12371  qnumdencl  12382  phiprmpw  12417  prmdiveq  12431  prm23lt5  12459  pcmpt  12539  infpnlem1  12555  oddennn  12636  nninfdclemf1  12696  imasaddfnlemg  13018  aprcotr  13919  cnpnei  14563  bl2in  14747  addcncntoplem  14905  rescncf  14925  limcresi  15010  cnplimcim  15011  efltlemlt  15118  ioocosf1o  15198  2lgslem1a1  15435  uzdcinzz  15552  bj-charfunbi  15565  bj-omssind  15689  bj-bdfindes  15703  bj-nntrans  15705  bj-nnelirr  15707  bj-omtrans  15710  setindis  15721  bdsetindis  15723  bj-inf2vnlem3  15726  bj-inf2vnlem4  15727  bj-findis  15733  bj-findes  15735