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  674  mtbii  676  orbi2d  792  pm3.11dc  960  prlem1  976  nfimd  1608  dral1  1753  cbvalv1  1774  cbvalh  1776  ax16i  1881  speiv  1885  a16g  1887  cbvalvw  1943  cbvexvw  1944  cleqh  2305  pm13.18  2457  rspcimdv  2878  rspcimedv  2879  rspcedv  2881  moi2  2954  moi  2956  eqrd  3211  abnexg  4493  ralxfrd  4509  ralxfr2d  4511  rexxfr2d  4512  elres  4995  2elresin  5387  f1ocnv  5535  tz6.12c  5606  fvun1  5645  dffo4  5728  isores3  5884  tposfo2  6353  issmo2  6375  iordsmo  6383  smoel2  6389  fiintim  7028  ismkvnex  7257  prarloclemarch  7531  genprndl  7634  genprndu  7635  ltpopr  7708  ltsopr  7709  recexprlem1ssl  7746  recexprlem1ssu  7747  aptiprlemu  7753  lttrsr  7875  aptap  8723  rerecapb  8916  nnmulcl  9057  nnnegz  9375  eluzdc  9731  negm  9736  iccid  10047  icoshft  10112  fzen  10165  elfz2nn0  10234  elfzom1p1elfzo  10343  flqeqceilz  10463  zmodidfzoimp  10499  swrd0g  11113  caucvgre  11292  qdenre  11513  dvdsval2  12101  negdvdsb  12118  muldvds2  12128  dvdsabseq  12158  bezoutlemaz  12324  bezoutlembz  12325  rplpwr  12348  alginv  12369  algfx  12374  coprmgcdb  12410  divgcdcoprm0  12423  prmgt1  12454  oddprmgt2  12456  rpexp1i  12476  2sqpwodd  12498  qnumdencl  12509  phiprmpw  12544  prmdiveq  12558  prm23lt5  12586  pcmpt  12666  infpnlem1  12682  oddennn  12763  nninfdclemf1  12823  imasaddfnlemg  13146  aprcotr  14047  cnpnei  14691  bl2in  14875  addcncntoplem  15033  rescncf  15053  limcresi  15138  cnplimcim  15139  efltlemlt  15246  ioocosf1o  15326  2lgslem1a1  15563  uzdcinzz  15734  bj-charfunbi  15747  bj-omssind  15871  bj-bdfindes  15885  bj-nntrans  15887  bj-nnelirr  15889  bj-omtrans  15892  setindis  15903  bdsetindis  15905  bj-inf2vnlem3  15908  bj-inf2vnlem4  15909  bj-findis  15915  bj-findes  15917