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  6567  ltsopr  6568  recexprlem1ssl  6603  recexprlem1ssu  6604  aptiprlemu  6610  lttrsr  6650  nnmulcl  7676  nnnegz  7984  eluzdc  8283  negm  8286  iccid  8524  icoshft  8588  fzen  8637  elfz2nn0  8703  elfzom1p1elfzo  8800  bj-omssind  9323  bj-bdfindes  9337  bj-nntrans  9339  bj-nnelirr  9341  bj-omtrans  9344  setindis  9351  bdsetindis  9353  bj-inf2vnlem3  9356  bj-inf2vnlem4  9357  bj-findis  9363  bj-findes  9365