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  1778  cbvalv1  1799  cbvalh  1801  ax16i  1906  speiv  1910  a16g  1912  cbvalvw  1968  cbvexvw  1969  cleqh  2331  pm13.18  2484  rspcimdv  2912  rspcimedv  2913  rspcedv  2915  moi2  2988  moi  2990  eqrd  3246  rabsnifsb  3741  abnexg  4549  ralxfrd  4565  ralxfr2d  4567  rexxfr2d  4568  elres  5055  2elresin  5450  f1ocnv  5605  tz6.12c  5678  fvun1  5721  dffo4  5803  isores3  5966  fvdifsuppst  6422  tposfo2  6476  issmo2  6498  iordsmo  6506  smoel2  6512  fiintim  7166  ismkvnex  7397  prarloclemarch  7681  genprndl  7784  genprndu  7785  ltpopr  7858  ltsopr  7859  recexprlem1ssl  7896  recexprlem1ssu  7897  aptiprlemu  7903  lttrsr  8025  aptap  8873  rerecapb  9066  nnmulcl  9207  nnnegz  9527  eluzdc  9889  negm  9894  iccid  10205  icoshft  10270  fzen  10323  elfz2nn0  10392  elfzom1p1elfzo  10505  flqeqceilz  10626  zmodidfzoimp  10662  swrd0g  11290  pfxccatin12lem2  11361  swrdccat  11365  swrdccat3blem  11369  caucvgre  11604  qdenre  11825  dvdsval2  12414  negdvdsb  12431  muldvds2  12441  dvdsabseq  12471  bezoutlemaz  12637  bezoutlembz  12638  rplpwr  12661  alginv  12682  algfx  12687  coprmgcdb  12723  divgcdcoprm0  12736  prmgt1  12767  oddprmgt2  12769  rpexp1i  12789  2sqpwodd  12811  qnumdencl  12822  phiprmpw  12857  prmdiveq  12871  prm23lt5  12899  pcmpt  12979  infpnlem1  12995  oddennn  13076  nninfdclemf1  13136  imasaddfnlemg  13460  aprcotr  14364  cnpnei  15013  bl2in  15197  addcncntoplem  15355  rescncf  15375  limcresi  15460  cnplimcim  15461  efltlemlt  15568  ioocosf1o  15648  2lgslem1a1  15888  clwwlkccatlem  16324  clwwlknonex2lem2  16362  uzdcinzz  16499  bj-charfunbi  16510  bj-omssind  16634  bj-bdfindes  16648  bj-nntrans  16650  bj-nnelirr  16652  bj-omtrans  16655  setindis  16666  bdsetindis  16668  bj-inf2vnlem3  16671  bj-inf2vnlem4  16672  bj-findis  16678  bj-findes  16680