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  679  mtbii  681  orbi2d  798  pm3.11dc  966  prlem1  982  nfimd  1634  dral1  1778  cbvalv1  1799  cbvalh  1801  ax16i  1906  speiv  1910  a16g  1912  cbvalvw  1968  cbvexvw  1969  cleqh  2331  pm13.18  2484  rspcimdv  2912  rspcimedv  2913  rspcedv  2915  moi2  2988  moi  2990  eqrd  3246  rabsnifsb  3741  abnexg  4549  ralxfrd  4565  ralxfr2d  4567  rexxfr2d  4568  elres  5055  2elresin  5450  f1ocnv  5605  tz6.12c  5678  fvun1  5721  dffo4  5803  isores3  5966  fvdifsuppst  6422  tposfo2  6476  issmo2  6498  iordsmo  6506  smoel2  6512  fiintim  7166  ismkvnex  7414  prarloclemarch  7698  genprndl  7801  genprndu  7802  ltpopr  7875  ltsopr  7876  recexprlem1ssl  7913  recexprlem1ssu  7914  aptiprlemu  7920  lttrsr  8042  aptap  8889  rerecapb  9082  nnmulcl  9223  nnnegz  9543  eluzdc  9905  negm  9910  iccid  10221  icoshft  10286  fzen  10340  elfz2nn0  10409  elfzom1p1elfzo  10522  flqeqceilz  10643  zmodidfzoimp  10679  swrd0g  11307  pfxccatin12lem2  11378  swrdccat  11382  swrdccat3blem  11386  caucvgre  11621  qdenre  11842  dvdsval2  12431  negdvdsb  12448  muldvds2  12458  dvdsabseq  12488  bezoutlemaz  12654  bezoutlembz  12655  rplpwr  12678  alginv  12699  algfx  12704  coprmgcdb  12740  divgcdcoprm0  12753  prmgt1  12784  oddprmgt2  12786  rpexp1i  12806  2sqpwodd  12828  qnumdencl  12839  phiprmpw  12874  prmdiveq  12888  prm23lt5  12916  pcmpt  12996  infpnlem1  13012  oddennn  13093  nninfdclemf1  13153  imasaddfnlemg  13477  aprcotr  14381  cnpnei  15030  bl2in  15214  addcncntoplem  15372  rescncf  15392  limcresi  15477  cnplimcim  15478  efltlemlt  15585  ioocosf1o  15665  2lgslem1a1  15905  clwwlkccatlem  16341  clwwlknonex2lem2  16379  uzdcinzz  16516  bj-charfunbi  16527  bj-omssind  16651  bj-bdfindes  16665  bj-nntrans  16667  bj-nnelirr  16669  bj-omtrans  16672  setindis  16683  bdsetindis  16685  bj-inf2vnlem3  16688  bj-inf2vnlem4  16689  bj-findis  16695  bj-findes  16697