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  662  mtbii  664  orbi2d  780  pm4.55dc  927  pm3.11dc  946  prlem1  962  nfimd  1572  dral1  1717  cbvalv1  1738  cbvalh  1740  ax16i  1845  speiv  1849  a16g  1851  cbvalvw  1906  cbvexvw  1907  cleqh  2264  pm13.18  2415  rspcimdv  2826  rspcimedv  2827  rspcedv  2829  moi2  2902  moi  2904  eqrd  3155  abnexg  4418  ralxfrd  4434  ralxfr2d  4436  rexxfr2d  4437  elres  4914  2elresin  5293  f1ocnv  5439  tz6.12c  5510  fvun1  5546  dffo4  5627  isores3  5777  tposfo2  6226  issmo2  6248  iordsmo  6256  smoel2  6262  fiintim  6885  ismkvnex  7110  prarloclemarch  7350  genprndl  7453  genprndu  7454  ltpopr  7527  ltsopr  7528  recexprlem1ssl  7565  recexprlem1ssu  7566  aptiprlemu  7572  lttrsr  7694  nnmulcl  8869  nnnegz  9185  eluzdc  9539  negm  9544  iccid  9852  icoshft  9917  fzen  9968  elfz2nn0  10037  elfzom1p1elfzo  10139  flqeqceilz  10243  zmodidfzoimp  10279  caucvgre  10909  qdenre  11130  dvdsval2  11716  negdvdsb  11733  muldvds2  11743  dvdsabseq  11770  bezoutlemaz  11921  bezoutlembz  11922  rplpwr  11945  alginv  11958  algfx  11963  coprmgcdb  11999  divgcdcoprm0  12012  prmgt1  12043  oddprmgt2  12045  rpexp1i  12063  2sqpwodd  12085  qnumdencl  12096  phiprmpw  12131  prmdiveq  12145  prm23lt5  12172  pcmpt  12250  oddennn  12262  nninfdclemf1  12324  cnpnei  12760  bl2in  12944  addcncntoplem  13092  rescncf  13109  limcresi  13176  cnplimcim  13177  efltlemlt  13236  ioocosf1o  13316  uzdcinzz  13514  bj-charfunbi  13528  bj-omssind  13652  bj-bdfindes  13666  bj-nntrans  13668  bj-nnelirr  13670  bj-omtrans  13673  setindis  13684  bdsetindis  13686  bj-inf2vnlem3  13689  bj-inf2vnlem4  13690  bj-findis  13696  bj-findes  13698