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  1737  equsex  1751  eleq1a  2277  ceqsalg  2800  cgsexg  2807  cgsex2g  2808  cgsex4g  2809  ceqsex  2810  spc2egv  2863  spc3egv  2865  csbiebt  3133  dfiin2g  3960  sotricim  4371  ralxfrALT  4515  iunpw  4528  opelxp  4706  ssrel  4764  ssrel2  4766  ssrelrel  4776  iss  5006  funcnvuni  5344  fun11iun  5545  tfrlem8  6406  eroveu  6715  fundmen  6900  nneneq  6956  fidifsnen  6969  prarloclem5  7615  prarloc  7618  recexprlemss1l  7750  recexprlemss1u  7751  uzin  9683  indstr  9716  elfzmlbp  10256  swrdnd  11115