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  981  ax11i  1760  equsex  1774  eleq1a  2301  ceqsalg  2829  cgsexg  2836  cgsex2g  2837  cgsex4g  2838  ceqsex  2839  spc2egv  2894  spc3egv  2896  csbiebt  3165  dfiin2g  4001  sotricim  4418  ralxfrALT  4562  iunpw  4575  opelxp  4753  ssrel  4812  ssrel2  4814  ssrelrel  4824  iss  5057  funcnvuni  5396  fun11iun  5601  tfrlem8  6479  eroveu  6790  fundmen  6976  nneneq  7038  fidifsnen  7052  prarloclem5  7710  prarloc  7713  recexprlemss1l  7845  recexprlemss1u  7846  uzin  9779  indstr  9817  elfzmlbp  10357  swrdnd  11230  isclwwlknx  16211