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  579  mtbid  584  mtbii  586  orbi2d  691  pm4.55dc  834  pm3.11dc  852  prlem1  868  nfimd  1459  dral1  1600  cbvalh  1618  ax16i  1720  speiv  1724  a16g  1726  cleqh  2119  pm13.18  2264  rspcimdv  2634  rspcimedv  2635  rspcedv  2637  moi2  2699  moi  2701  eqrd  2940  ralxfrd  4144  ralxfr2d  4146  rexxfr2d  4147  elres  4573  2elresin  4936  f1ocnv  5064  tz6.12c  5128  fvun1  5164  dffo4  5240  isores3  5380  tposfo2  5804  issmo2  5826  iordsmo  5834  smoel2  5840  prarloclemarch  6275  genprndl  6376  genprndu  6377  ltpopr  6432  ltsopr  6433  recexprlem1ssl  6467  recexprlem1ssu  6468  lttrsr  6509  bj-omssind  7304  bj-bdfindes  7318  bj-nntrans  7320  bj-nnelirr  7322  bj-omtrans  7325  setindis  7332  bdsetindis  7334  bj-inf2vnlem3  7337  bj-inf2vnlem4  7338  bj-findis  7344  bj-findes  7346