Theorem biimprcd 159

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 156	1 ⊢ (𝜒 → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimparc  297  pm5.32  449  oplem1  960  ax11i  1693  equsex  1707  eleq1a  2212  ceqsalg  2717  cgsexg  2724  cgsex2g  2725  cgsex4g  2726  ceqsex  2727  spc2egv  2779  spc3egv  2781  csbiebt  3044  dfiin2g  3854  sotricim  4253  ralxfrALT  4396  iunpw  4409  opelxp  4577  ssrel  4635  ssrel2  4637  ssrelrel  4647  iss  4873  funcnvuni  5200  fun11iun  5396  tfrlem8  6223  eroveu  6528  fundmen  6708  nneneq  6759  fidifsnen  6772  prarloclem5  7332  prarloc  7335  recexprlemss1l  7467  recexprlemss1u  7468  uzin  9382  indstr  9415  elfzmlbp  9940