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  457  oplem1  988  ax11i  1766  equsex  1780  eleq1a  2310  ceqsalg  2850  cgsexg  2857  cgsex2g  2858  cgsex4g  2859  ceqsex  2860  spc2egv  2915  spc3egv  2917  csbiebt  3187  dfiin2g  4040  sotricim  4463  ralxfrALT  4608  iunpw  4621  opelxp  4799  ssrel  4858  ssrel2  4860  ssrelrel  4870  iss  5104  funcnvuni  5445  fun11iun  5655  tfrlem8  6579  eroveu  6890  fundmen  7084  nneneq  7148  fidifsnen  7162  prarloclem5  7857  prarloc  7860  recexprlemss1l  7992  recexprlemss1u  7993  uzin  9934  indstr  9972  elfzmlbp  10517  swrdnd  11409  isclwwlknx  16571