Theorem biimprcd 149

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

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  biimparc  283  pm5.32  426  oplem1  882  ax11i  1602  equsex  1616  eleq1a  2109  ceqsalg  2582  cgsexg  2589  cgsex2g  2590  cgsex4g  2591  ceqsex  2592  spc2egv  2642  spc3egv  2644  csbiebt  2886  dfiin2g  3690  sotricim  4060  ralxfrALT  4199  iunpw  4211  opelxp  4374  ssrel  4428  ssrel2  4430  ssrelrel  4440  iss  4654  funcnvuni  4968  fun11iun  5147  tfrlem8  5934  eroveu  6197  fundmen  6286  nneneq  6320  fidifsnen  6331  prarloclem5  6598  prarloc  6601  recexprlemss1l  6733  recexprlemss1u  6734  uzin  8505  indstr  8536  elfzmlbp  8990