Theorem biimprcd 158

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

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  biimparc  293  pm5.32  441  oplem1  921  ax11i  1649  equsex  1663  eleq1a  2159  ceqsalg  2647  cgsexg  2654  cgsex2g  2655  cgsex4g  2656  ceqsex  2657  spc2egv  2708  spc3egv  2710  csbiebt  2967  dfiin2g  3763  sotricim  4150  ralxfrALT  4289  iunpw  4302  opelxp  4467  ssrel  4526  ssrel2  4528  ssrelrel  4538  iss  4758  funcnvuni  5083  fun11iun  5274  tfrlem8  6083  eroveu  6381  fundmen  6521  nneneq  6571  fidifsnen  6584  prarloclem5  7057  prarloc  7060  recexprlemss1l  7192  recexprlemss1u  7193  uzin  9049  indstr  9079  elfzmlbp  9539