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  576  mtbid  581  mtbii  583  orbi2d  688  pm4.55dc  830  pm3.11dc  848  prlem1  864  nfimd  1453  dral1  1594  cbvalh  1612  ax16i  1714  speiv  1718  a16g  1720  cleqh  2113  pm13.18  2258  rspcimdv  2628  rspcimedv  2629  rspcedv  2631  moi2  2693  moi  2695  eqrd  2934  ralxfrd  4135  ralxfr2d  4137  rexxfr2d  4138  elres  4564  2elresin  4927  f1ocnv  5055  tz6.12c  5119  fvun1  5155  dffo4  5231  isores3  5371  tposfo2  5795  issmo2  5817  iordsmo  5825  smoel2  5831  prarloclemarch  6264  genprndl  6365  genprndu  6366  ltpopr  6421  ltsopr  6422  recexprlem1ssl  6457  recexprlem1ssu  6458  aptiprlemu  6464  lttrsr  6503  nnmulcl  7521  nnnegz  7825  iccid  8273  icoshft  8337  bj-omssind  8511  bj-bdfindes  8525  bj-nntrans  8527  bj-nnelirr  8529  bj-omtrans  8532  setindis  8539  bdsetindis  8541  bj-inf2vnlem3  8544  bj-inf2vnlem4  8545  bj-findis  8551  bj-findes  8553