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  2278  ceqsalg  2802  cgsexg  2809  cgsex2g  2810  cgsex4g  2811  ceqsex  2812  spc2egv  2867  spc3egv  2869  csbiebt  3137  dfiin2g  3965  sotricim  4377  ralxfrALT  4521  iunpw  4534  opelxp  4712  ssrel  4770  ssrel2  4772  ssrelrel  4782  iss  5013  funcnvuni  5351  fun11iun  5554  tfrlem8  6416  eroveu  6725  fundmen  6911  nneneq  6968  fidifsnen  6981  prarloclem5  7628  prarloc  7631  recexprlemss1l  7763  recexprlemss1u  7764  uzin  9696  indstr  9729  elfzmlbp  10269  swrdnd  11130