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:  syl6bir  164  mpbird  167  sylibrd  169  sylbird  170  imbi1d  231  biimpar  297  mtbid  673  mtbii  675  orbi2d  791  pm4.55dc  939  pm3.11dc  958  prlem1  974  nfimd  1595  dral1  1740  cbvalv1  1761  cbvalh  1763  ax16i  1868  speiv  1872  a16g  1874  cbvalvw  1929  cbvexvw  1930  cleqh  2287  pm13.18  2438  rspcimdv  2854  rspcimedv  2855  rspcedv  2857  moi2  2930  moi  2932  eqrd  3185  abnexg  4458  ralxfrd  4474  ralxfr2d  4476  rexxfr2d  4477  elres  4955  2elresin  5339  f1ocnv  5486  tz6.12c  5557  fvun1  5595  dffo4  5677  isores3  5829  tposfo2  6282  issmo2  6304  iordsmo  6312  smoel2  6318  fiintim  6942  ismkvnex  7167  prarloclemarch  7431  genprndl  7534  genprndu  7535  ltpopr  7608  ltsopr  7609  recexprlem1ssl  7646  recexprlem1ssu  7647  aptiprlemu  7653  lttrsr  7775  aptap  8621  rerecapb  8814  nnmulcl  8954  nnnegz  9270  eluzdc  9624  negm  9629  iccid  9939  icoshft  10004  fzen  10057  elfz2nn0  10126  elfzom1p1elfzo  10228  flqeqceilz  10332  zmodidfzoimp  10368  caucvgre  11004  qdenre  11225  dvdsval2  11811  negdvdsb  11828  muldvds2  11838  dvdsabseq  11867  bezoutlemaz  12018  bezoutlembz  12019  rplpwr  12042  alginv  12061  algfx  12066  coprmgcdb  12102  divgcdcoprm0  12115  prmgt1  12146  oddprmgt2  12148  rpexp1i  12168  2sqpwodd  12190  qnumdencl  12201  phiprmpw  12236  prmdiveq  12250  prm23lt5  12277  pcmpt  12355  infpnlem1  12371  oddennn  12407  nninfdclemf1  12467  imasaddfnlemg  12753  aprcotr  13531  cnpnei  14072  bl2in  14256  addcncntoplem  14404  rescncf  14421  limcresi  14488  cnplimcim  14489  efltlemlt  14548  ioocosf1o  14628  uzdcinzz  14903  bj-charfunbi  14916  bj-omssind  15040  bj-bdfindes  15054  bj-nntrans  15056  bj-nnelirr  15058  bj-omtrans  15061  setindis  15072  bdsetindis  15074  bj-inf2vnlem3  15077  bj-inf2vnlem4  15078  bj-findis  15084  bj-findes  15086