Theorem biimprd 147

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 145	1 ⊢ (φ → (χ → ψ))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  syl6bir  153  mpbird  156  sylibrd  158  sylbird  159  imbi1d  220  biimpar  281  notbid  591  mtbid  596  mtbii  598  orbi2d  703  pm4.55dc  845  pm3.11dc  863  prlem1  879  nfimd  1474  dral1  1615  cbvalh  1633  ax16i  1735  speiv  1739  a16g  1741  cleqh  2134  pm13.18  2280  rspcimdv  2651  rspcimedv  2652  rspcedv  2654  moi2  2716  moi  2718  eqrd  2957  ralxfrd  4160  ralxfr2d  4162  rexxfr2d  4163  elres  4589  2elresin  4953  f1ocnv  5082  tz6.12c  5146  fvun1  5182  dffo4  5258  isores3  5398  tposfo2  5823  issmo2  5845  iordsmo  5853  smoel2  5859  prarloclemarch  6401  genprndl  6504  genprndu  6505  ltpopr  6569  ltsopr  6570  recexprlem1ssl  6605  recexprlem1ssu  6606  aptiprlemu  6612  lttrsr  6690  nnmulcl  7716  nnnegz  8024  eluzdc  8323  negm  8326  iccid  8564  icoshft  8628  fzen  8677  elfz2nn0  8743  elfzom1p1elfzo  8840  bj-omssind  9394  bj-bdfindes  9409  bj-nntrans  9411  bj-nnelirr  9413  bj-omtrans  9416  setindis  9427  bdsetindis  9429  bj-inf2vnlem3  9432  bj-inf2vnlem4  9433  bj-findis  9439  bj-findes  9441