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  1609  dral1  1754  cbvalv1  1775  cbvalh  1777  ax16i  1882  speiv  1886  a16g  1888  cbvalvw  1944  cbvexvw  1945  cleqh  2307  pm13.18  2459  rspcimdv  2885  rspcimedv  2886  rspcedv  2888  moi2  2961  moi  2963  eqrd  3219  abnexg  4511  ralxfrd  4527  ralxfr2d  4529  rexxfr2d  4530  elres  5014  2elresin  5406  f1ocnv  5557  tz6.12c  5629  fvun1  5668  dffo4  5751  isores3  5907  tposfo2  6376  issmo2  6398  iordsmo  6406  smoel2  6412  fiintim  7054  ismkvnex  7283  prarloclemarch  7566  genprndl  7669  genprndu  7670  ltpopr  7743  ltsopr  7744  recexprlem1ssl  7781  recexprlem1ssu  7782  aptiprlemu  7788  lttrsr  7910  aptap  8758  rerecapb  8951  nnmulcl  9092  nnnegz  9410  eluzdc  9766  negm  9771  iccid  10082  icoshft  10147  fzen  10200  elfz2nn0  10269  elfzom1p1elfzo  10380  flqeqceilz  10500  zmodidfzoimp  10536  swrd0g  11151  pfxccatin12lem2  11222  swrdccat  11226  swrdccat3blem  11230  caucvgre  11407  qdenre  11628  dvdsval2  12216  negdvdsb  12233  muldvds2  12243  dvdsabseq  12273  bezoutlemaz  12439  bezoutlembz  12440  rplpwr  12463  alginv  12484  algfx  12489  coprmgcdb  12525  divgcdcoprm0  12538  prmgt1  12569  oddprmgt2  12571  rpexp1i  12591  2sqpwodd  12613  qnumdencl  12624  phiprmpw  12659  prmdiveq  12673  prm23lt5  12701  pcmpt  12781  infpnlem1  12797  oddennn  12878  nninfdclemf1  12938  imasaddfnlemg  13261  aprcotr  14162  cnpnei  14806  bl2in  14990  addcncntoplem  15148  rescncf  15168  limcresi  15253  cnplimcim  15254  efltlemlt  15361  ioocosf1o  15441  2lgslem1a1  15678  uzdcinzz  15934  bj-charfunbi  15946  bj-omssind  16070  bj-bdfindes  16084  bj-nntrans  16086  bj-nnelirr  16088  bj-omtrans  16091  setindis  16102  bdsetindis  16104  bj-inf2vnlem3  16107  bj-inf2vnlem4  16108  bj-findis  16114  bj-findes  16116