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  661  mtbii  663  orbi2d  779  pm4.55dc  922  pm3.11dc  941  prlem1  957  nfimd  1564  dral1  1708  cbvalh  1726  ax16i  1830  speiv  1834  a16g  1836  cleqh  2239  pm13.18  2389  rspcimdv  2790  rspcimedv  2791  rspcedv  2793  moi2  2865  moi  2867  eqrd  3115  abnexg  4367  ralxfrd  4383  ralxfr2d  4385  rexxfr2d  4386  elres  4855  2elresin  5234  f1ocnv  5380  tz6.12c  5451  fvun1  5487  dffo4  5568  isores3  5716  tposfo2  6164  issmo2  6186  iordsmo  6194  smoel2  6200  fiintim  6817  ismkvnex  7029  prarloclemarch  7226  genprndl  7329  genprndu  7330  ltpopr  7403  ltsopr  7404  recexprlem1ssl  7441  recexprlem1ssu  7442  aptiprlemu  7448  lttrsr  7570  nnmulcl  8741  nnnegz  9057  eluzdc  9404  negm  9407  iccid  9708  icoshft  9773  fzen  9823  elfz2nn0  9892  elfzom1p1elfzo  9991  flqeqceilz  10091  zmodidfzoimp  10127  caucvgre  10753  qdenre  10974  dvdsval2  11496  negdvdsb  11509  muldvds2  11519  dvdsabseq  11545  bezoutlemaz  11691  bezoutlembz  11692  rplpwr  11715  alginv  11728  algfx  11733  coprmgcdb  11769  divgcdcoprm0  11782  prmgt1  11812  oddprmgt2  11814  rpexp1i  11832  2sqpwodd  11854  qnumdencl  11865  phiprmpw  11898  oddennn  11905  cnpnei  12388  bl2in  12572  addcncntoplem  12720  rescncf  12737  limcresi  12804  cnplimcim  12805  uzdcinzz  13005  bj-omssind  13133  bj-bdfindes  13147  bj-nntrans  13149  bj-nnelirr  13151  bj-omtrans  13154  setindis  13165  bdsetindis  13167  bj-inf2vnlem3  13170  bj-inf2vnlem4  13171  bj-findis  13177  bj-findes  13179