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  440  oplem1  916  ax11i  1642  equsex  1656  eleq1a  2150  ceqsalg  2627  cgsexg  2634  cgsex2g  2635  cgsex4g  2636  ceqsex  2637  spc2egv  2687  spc3egv  2689  csbiebt  2942  dfiin2g  3711  sotricim  4078  ralxfrALT  4217  iunpw  4229  opelxp  4392  ssrel  4446  ssrel2  4448  ssrelrel  4458  iss  4674  funcnvuni  4988  fun11iun  5167  tfrlem8  5957  eroveu  6220  fundmen  6309  nneneq  6343  fidifsnen  6355  prarloclem5  6690  prarloc  6693  recexprlemss1l  6825  recexprlemss1u  6826  uzin  8651  indstr  8681  elfzmlbp  9143