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  678  mtbii  680  orbi2d  797  pm3.11dc  965  prlem1  981  nfimd  1633  dral1  1778  cbvalv1  1799  cbvalh  1801  ax16i  1906  speiv  1910  a16g  1912  cbvalvw  1968  cbvexvw  1969  cleqh  2331  pm13.18  2483  rspcimdv  2911  rspcimedv  2912  rspcedv  2914  moi2  2987  moi  2989  eqrd  3245  rabsnifsb  3737  abnexg  4543  ralxfrd  4559  ralxfr2d  4561  rexxfr2d  4562  elres  5049  2elresin  5443  f1ocnv  5596  tz6.12c  5669  fvun1  5712  dffo4  5795  isores3  5955  tposfo2  6432  issmo2  6454  iordsmo  6462  smoel2  6468  fiintim  7122  ismkvnex  7353  prarloclemarch  7637  genprndl  7740  genprndu  7741  ltpopr  7814  ltsopr  7815  recexprlem1ssl  7852  recexprlem1ssu  7853  aptiprlemu  7859  lttrsr  7981  aptap  8829  rerecapb  9022  nnmulcl  9163  nnnegz  9481  eluzdc  9843  negm  9848  iccid  10159  icoshft  10224  fzen  10277  elfz2nn0  10346  elfzom1p1elfzo  10458  flqeqceilz  10579  zmodidfzoimp  10615  swrd0g  11240  pfxccatin12lem2  11311  swrdccat  11315  swrdccat3blem  11319  caucvgre  11541  qdenre  11762  dvdsval2  12350  negdvdsb  12367  muldvds2  12377  dvdsabseq  12407  bezoutlemaz  12573  bezoutlembz  12574  rplpwr  12597  alginv  12618  algfx  12623  coprmgcdb  12659  divgcdcoprm0  12672  prmgt1  12703  oddprmgt2  12705  rpexp1i  12725  2sqpwodd  12747  qnumdencl  12758  phiprmpw  12793  prmdiveq  12807  prm23lt5  12835  pcmpt  12915  infpnlem1  12931  oddennn  13012  nninfdclemf1  13072  imasaddfnlemg  13396  aprcotr  14298  cnpnei  14942  bl2in  15126  addcncntoplem  15284  rescncf  15304  limcresi  15389  cnplimcim  15390  efltlemlt  15497  ioocosf1o  15577  2lgslem1a1  15814  clwwlkccatlem  16250  clwwlknonex2lem2  16288  uzdcinzz  16394  bj-charfunbi  16406  bj-omssind  16530  bj-bdfindes  16544  bj-nntrans  16546  bj-nnelirr  16548  bj-omtrans  16551  setindis  16562  bdsetindis  16564  bj-inf2vnlem3  16567  bj-inf2vnlem4  16568  bj-findis  16574  bj-findes  16576