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  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  3684  rabsnifsb  3773  abnexg  4587  ralxfrd  4603  ralxfr2d  4605  rexxfr2d  4606  elres  5094  2elresin  5489  f1ocnv  5647  tz6.12c  5720  fvun1  5763  dffo4  5847  isores3  6011  fvdifsuppst  6474  tposfo2  6528  issmo2  6550  iordsmo  6558  smoel2  6564  fiintim  7228  ismkvnex  7485  prarloclemarch  7775  genprndl  7878  genprndu  7879  ltpopr  7952  ltsopr  7953  recexprlem1ssl  7990  recexprlem1ssu  7991  aptiprlemu  7997  lttrsr  8119  aptap  8968  rerecapb  9163  nnmulcl  9304  nnnegz  9626  eluzdc  9989  negm  9994  iccid  10306  icoshft  10371  fzen  10426  elfz2nn0  10497  elfzom1p1elfzo  10610  flqeqceilz  10733  zmodidfzoimp  10769  swrd0g  11410  pfxccatin12lem2  11481  swrdccat  11485  swrdccat3blem  11489  caucvgre  11725  qdenre  11946  dvdsval2  12535  negdvdsb  12552  muldvds2  12562  dvdsabseq  12592  bezoutlemaz  12758  bezoutlembz  12759  rplpwr  12782  alginv  12803  algfx  12808  coprmgcdb  12844  divgcdcoprm0  12857  prmgt1  12888  oddprmgt2  12890  rpexp1i  12910  2sqpwodd  12932  qnumdencl  12943  phiprmpw  12978  prmdiveq  12992  prm23lt5  13020  pcmpt  13100  infpnlem1  13116  oddennn  13261  nninfdclemf1  13321  imasaddfnlemg  13612  aprcotr  14570  cnpnei  15243  bl2in  15427  addcncntoplem  15585  rescncf  15605  limcresi  15690  cnplimcim  15691  efltlemlt  15798  ioocosf1o  15878  2lgslem1a1  16119  clwwlkccatlem  16555  clwwlknonex2lem2  16593  uzdcinzz  16740  bj-charfunbi  16751  bj-omssind  16875  bj-bdfindes  16889  bj-nntrans  16891  bj-nnelirr  16893  bj-omtrans  16896  setindis  16907  bdsetindis  16909  bj-inf2vnlem3  16912  bj-inf2vnlem4  16913  bj-findis  16919  bj-findes  16921