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-1 5  ax-2 6  ax-mp 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  293  mtbid  644  mtbii  646  orbi2d  762  pm4.55dc  905  pm3.11dc  924  prlem1  940  nfimd  1547  dral1  1691  cbvalh  1709  ax16i  1812  speiv  1816  a16g  1818  cleqh  2214  pm13.18  2363  rspcimdv  2761  rspcimedv  2762  rspcedv  2764  moi2  2834  moi  2836  eqrd  3081  abnexg  4327  ralxfrd  4343  ralxfr2d  4345  rexxfr2d  4346  elres  4813  2elresin  5192  f1ocnv  5336  tz6.12c  5405  fvun1  5441  dffo4  5522  isores3  5670  tposfo2  6118  issmo2  6140  iordsmo  6148  smoel2  6154  fiintim  6770  ismkvnex  6979  prarloclemarch  7174  genprndl  7277  genprndu  7278  ltpopr  7351  ltsopr  7352  recexprlem1ssl  7389  recexprlem1ssu  7390  aptiprlemu  7396  lttrsr  7505  nnmulcl  8651  nnnegz  8961  eluzdc  9306  negm  9309  iccid  9601  icoshft  9666  fzen  9716  elfz2nn0  9785  elfzom1p1elfzo  9884  flqeqceilz  9984  zmodidfzoimp  10020  caucvgre  10645  qdenre  10866  dvdsval2  11344  negdvdsb  11357  muldvds2  11367  dvdsabseq  11393  bezoutlemaz  11537  bezoutlembz  11538  rplpwr  11561  alginv  11574  algfx  11579  coprmgcdb  11615  divgcdcoprm0  11628  prmgt1  11658  oddprmgt2  11660  rpexp1i  11678  2sqpwodd  11699  qnumdencl  11710  phiprmpw  11743  oddennn  11750  cnpnei  12230  bl2in  12392  addcncntoplem  12537  rescncf  12554  limcresi  12591  cnplimcim  12592  uzdcinzz  12697  bj-omssind  12825  bj-bdfindes  12839  bj-nntrans  12841  bj-nnelirr  12843  bj-omtrans  12846  setindis  12857  bdsetindis  12859  bj-inf2vnlem3  12862  bj-inf2vnlem4  12863  bj-findis  12869  bj-findes  12871