Theorem biimprcd 160

Description: Deduce a converse commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)

Hypothesis

Ref	Expression
biimpcd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimprcd	⊢ (𝜒 → (𝜑 → 𝜓))

Proof of Theorem biimprcd

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜒 → 𝜒)
2		biimpcd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	syl5ibrcom 157	1 ⊢ (𝜒 → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biimparc  299  pm5.32  453  oplem1  978  ax11i  1738  equsex  1752  eleq1a  2279  ceqsalg  2805  cgsexg  2812  cgsex2g  2813  cgsex4g  2814  ceqsex  2815  spc2egv  2870  spc3egv  2872  csbiebt  3141  dfiin2g  3974  sotricim  4388  ralxfrALT  4532  iunpw  4545  opelxp  4723  ssrel  4781  ssrel2  4783  ssrelrel  4793  iss  5024  funcnvuni  5362  fun11iun  5565  tfrlem8  6427  eroveu  6736  fundmen  6922  nneneq  6979  fidifsnen  6993  prarloclem5  7648  prarloc  7651  recexprlemss1l  7783  recexprlemss1u  7784  uzin  9716  indstr  9749  elfzmlbp  10289  swrdnd  11150