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  3201  abnexg  4481  ralxfrd  4497  ralxfr2d  4499  rexxfr2d  4500  elres  4982  2elresin  5369  f1ocnv  5517  tz6.12c  5588  fvun1  5627  dffo4  5710  isores3  5862  tposfo2  6325  issmo2  6347  iordsmo  6355  smoel2  6361  fiintim  6992  ismkvnex  7221  prarloclemarch  7485  genprndl  7588  genprndu  7589  ltpopr  7662  ltsopr  7663  recexprlem1ssl  7700  recexprlem1ssu  7701  aptiprlemu  7707  lttrsr  7829  aptap  8677  rerecapb  8870  nnmulcl  9011  nnnegz  9329  eluzdc  9684  negm  9689  iccid  10000  icoshft  10065  fzen  10118  elfz2nn0  10187  elfzom1p1elfzo  10290  flqeqceilz  10410  zmodidfzoimp  10446  caucvgre  11146  qdenre  11367  dvdsval2  11955  negdvdsb  11972  muldvds2  11982  dvdsabseq  12012  bezoutlemaz  12170  bezoutlembz  12171  rplpwr  12194  alginv  12215  algfx  12220  coprmgcdb  12256  divgcdcoprm0  12269  prmgt1  12300  oddprmgt2  12302  rpexp1i  12322  2sqpwodd  12344  qnumdencl  12355  phiprmpw  12390  prmdiveq  12404  prm23lt5  12432  pcmpt  12512  infpnlem1  12528  oddennn  12609  nninfdclemf1  12669  imasaddfnlemg  12957  aprcotr  13841  cnpnei  14455  bl2in  14639  addcncntoplem  14797  rescncf  14817  limcresi  14902  cnplimcim  14903  efltlemlt  15010  ioocosf1o  15090  2lgslem1a1  15327  uzdcinzz  15444  bj-charfunbi  15457  bj-omssind  15581  bj-bdfindes  15595  bj-nntrans  15597  bj-nnelirr  15599  bj-omtrans  15602  setindis  15613  bdsetindis  15615  bj-inf2vnlem3  15618  bj-inf2vnlem4  15619  bj-findis  15625  bj-findes  15627