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  7495  prarloclemarch  7785  genprndl  7888  genprndu  7889  ltpopr  7962  ltsopr  7963  recexprlem1ssl  8000  recexprlem1ssu  8001  aptiprlemu  8007  lttrsr  8129  aptap  8978  rerecapb  9173  nnmulcl  9325  nnnegz  9647  eluzdc  10010  negm  10015  iccid  10327  icoshft  10392  fzen  10447  elfz2nn0  10519  elfzom1p1elfzo  10632  flqeqceilz  10755  zmodidfzoimp  10791  swrd0g  11432  pfxccatin12lem2  11503  swrdccat  11507  swrdccat3blem  11511  caucvgre  11747  qdenre  11968  dvdsval2  12557  negdvdsb  12574  muldvds2  12584  dvdsabseq  12614  bezoutlemaz  12780  bezoutlembz  12781  rplpwr  12804  alginv  12825  algfx  12830  coprmgcdb  12866  divgcdcoprm0  12879  prmgt1  12910  oddprmgt2  12912  rpexp1i  12932  2sqpwodd  12954  qnumdencl  12965  phiprmpw  13000  prmdiveq  13014  prm23lt5  13042  pcmpt  13122  infpnlem1  13138  oddennn  13283  nninfdclemf1  13343  imasaddfnlemg  13635  aprcotr  14597  cnpnei  15320  bl2in  15504  addcncntoplem  15662  rescncf  15682  limcresi  15767  cnplimcim  15768  efltlemlt  15875  ioocosf1o  15955  2lgslem1a1  16205  clwwlkccatlem  16641  clwwlknonex2lem2  16679  uzdcinzz  16826  bj-charfunbi  16837  bj-omssind  16961  bj-bdfindes  16975  bj-nntrans  16977  bj-nnelirr  16979  bj-omtrans  16982  setindis  16993  bdsetindis  16995  bj-inf2vnlem3  16998  bj-inf2vnlem4  16999  bj-findis  17005  bj-findes  17007