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 ⊢ (𝜑 → (𝜒 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimtrrdi  164  mpbird  167  sylibrd  169  sylbird  170  imbi1d  231  biimpar  297  mtbid  683  mtbii  685  orbi2d  802  pm3.11dc  970  prlem1  986  nfimd  1638  dral1  1783  cbvalv1  1804  cbvalh  1806  ax16i  1911  speiv  1915  a16g  1917  cbvalvw  1975  cbvexvw  1976  cleqh  2338  pm13.18  2501  rspcimdv  2930  rspcimedv  2931  rspcedv  2933  moi2  3007  moi  3009  eqrd  3266  ifeqeqxdc  3687  rabsnifsb  3777  abnexg  4592  ralxfrd  4608  ralxfr2d  4610  rexxfr2d  4611  elres  5099  2elresin  5494  f1ocnv  5652  tz6.12c  5725  fvun1  5769  dffo4  5856  isores3  6021  fvdifsuppst  6484  tposfo2  6538  issmo2  6560  iordsmo  6568  smoel2  6574  fiintim  7238  ismkvnex  7496  prarloclemarch  7786  genprndl  7889  genprndu  7890  ltpopr  7963  ltsopr  7964  recexprlem1ssl  8001  recexprlem1ssu  8002  aptiprlemu  8008  lttrsr  8130  aptap  8981  rerecapb  9176  nnmulcl  9328  nnnegz  9652  eluzdc  10020  negm  10025  iccid  10338  icoshft  10403  fzen  10458  elfz2nn0  10530  elfzom1p1elfzo  10643  flqeqceilz  10770  zmodidfzoimp  10806  swrd0g  11448  pfxccatin12lem2  11519  swrdccat  11523  swrdccat3blem  11527  caucvgre  11763  qdenre  11985  dvdsval2  12576  negdvdsb  12593  muldvds2  12603  dvdsabseq  12633  bezoutlemaz  12799  bezoutlembz  12800  rplpwr  12823  alginv  12844  algfx  12849  coprmgcdb  12885  divgcdcoprm0  12898  prmgt1  12930  oddprmgt2  12932  rpexp1i  12952  2sqpwodd  12975  qnumdencl  12986  phiprmpw  13023  prmdiveq  13037  prm23lt5  13065  pcmpt  13145  infpnlem1  13161  oddennn  13335  nninfdclemf1  13395  imasaddfnlemg  13688  aprcotr  14681  cnpnei  15411  bl2in  15595  addcncntoplem  15753  rescncf  15773  limcresi  15858  cnplimcim  15859  efltlemlt  15966  ioocosf1o  16047  bposlem1  16272  bposlem5  16276  2lgslem1a1  16371  clwwlkccatlem  16807  clwwlknonex2lem2  16845  uzdcinzz  16992  bj-charfunbi  17003  bj-omssind  17127  bj-bdfindes  17141  bj-nntrans  17143  bj-nnelirr  17145  bj-omtrans  17148  setindis  17159  bdsetindis  17161  bj-inf2vnlem3  17164  bj-inf2vnlem4  17165  bj-findis  17171  bj-findes  17173