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  2828  cgsexg  2835  cgsex2g  2836  cgsex4g  2837  ceqsex  2838  spc2egv  2893  spc3egv  2895  csbiebt  3164  dfiin2g  3998  sotricim  4414  ralxfrALT  4558  iunpw  4571  opelxp  4749  ssrel  4807  ssrel2  4809  ssrelrel  4819  iss  5051  funcnvuni  5390  fun11iun  5593  tfrlem8  6464  eroveu  6773  fundmen  6959  nneneq  7018  fidifsnen  7032  prarloclem5  7687  prarloc  7690  recexprlemss1l  7822  recexprlemss1u  7823  uzin  9755  indstr  9788  elfzmlbp  10328  swrdnd  11191