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  984  ax11i  1762  equsex  1776  eleq1a  2306  ceqsalg  2844  cgsexg  2851  cgsex2g  2852  cgsex4g  2853  ceqsex  2854  spc2egv  2909  spc3egv  2911  csbiebt  3181  dfiin2g  4029  sotricim  4449  ralxfrALT  4593  iunpw  4606  opelxp  4784  ssrel  4843  ssrel2  4845  ssrelrel  4855  iss  5089  funcnvuni  5430  fun11iun  5640  tfrlem8  6562  eroveu  6873  fundmen  7060  nneneq  7124  fidifsnen  7138  prarloclem5  7831  prarloc  7834  recexprlemss1l  7966  recexprlemss1u  7967  uzin  9905  indstr  9943  elfzmlbp  10488  swrdnd  11376  isclwwlknx  16537