Theorem biimprd 157

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	syl5ibr 155	1 ⊢ (𝜑 → (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl6bir  163  mpbird  166  sylibrd  168  sylbird  169  imbi1d  230  biimpar  295  mtbid  667  mtbii  669  orbi2d  785  pm4.55dc  933  pm3.11dc  952  prlem1  968  nfimd  1578  dral1  1723  cbvalv1  1744  cbvalh  1746  ax16i  1851  speiv  1855  a16g  1857  cbvalvw  1912  cbvexvw  1913  cleqh  2270  pm13.18  2421  rspcimdv  2835  rspcimedv  2836  rspcedv  2838  moi2  2911  moi  2913  eqrd  3165  abnexg  4429  ralxfrd  4445  ralxfr2d  4447  rexxfr2d  4448  elres  4925  2elresin  5307  f1ocnv  5453  tz6.12c  5524  fvun1  5560  dffo4  5641  isores3  5791  tposfo2  6243  issmo2  6265  iordsmo  6273  smoel2  6279  fiintim  6902  ismkvnex  7127  prarloclemarch  7367  genprndl  7470  genprndu  7471  ltpopr  7544  ltsopr  7545  recexprlem1ssl  7582  recexprlem1ssu  7583  aptiprlemu  7589  lttrsr  7711  nnmulcl  8886  nnnegz  9202  eluzdc  9556  negm  9561  iccid  9869  icoshft  9934  fzen  9986  elfz2nn0  10055  elfzom1p1elfzo  10157  flqeqceilz  10261  zmodidfzoimp  10297  caucvgre  10932  qdenre  11153  dvdsval2  11739  negdvdsb  11756  muldvds2  11766  dvdsabseq  11794  bezoutlemaz  11945  bezoutlembz  11946  rplpwr  11969  alginv  11988  algfx  11993  coprmgcdb  12029  divgcdcoprm0  12042  prmgt1  12073  oddprmgt2  12075  rpexp1i  12095  2sqpwodd  12117  qnumdencl  12128  phiprmpw  12163  prmdiveq  12177  prm23lt5  12204  pcmpt  12282  infpnlem1  12298  oddennn  12334  nninfdclemf1  12394  cnpnei  12972  bl2in  13156  addcncntoplem  13304  rescncf  13321  limcresi  13388  cnplimcim  13389  efltlemlt  13448  ioocosf1o  13528  uzdcinzz  13792  bj-charfunbi  13806  bj-omssind  13930  bj-bdfindes  13944  bj-nntrans  13946  bj-nnelirr  13948  bj-omtrans  13951  setindis  13962  bdsetindis  13964  bj-inf2vnlem3  13967  bj-inf2vnlem4  13968  bj-findis  13974  bj-findes  13976