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  977  ax11i  1728  equsex  1742  eleq1a  2268  ceqsalg  2791  cgsexg  2798  cgsex2g  2799  cgsex4g  2800  ceqsex  2801  spc2egv  2854  spc3egv  2856  csbiebt  3124  dfiin2g  3949  sotricim  4358  ralxfrALT  4502  iunpw  4515  opelxp  4693  ssrel  4751  ssrel2  4753  ssrelrel  4763  iss  4992  funcnvuni  5327  fun11iun  5525  tfrlem8  6376  eroveu  6685  fundmen  6865  nneneq  6918  fidifsnen  6931  prarloclem5  7567  prarloc  7570  recexprlemss1l  7702  recexprlemss1u  7703  uzin  9634  indstr  9667  elfzmlbp  10207