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  978  ax11i  1737  equsex  1751  eleq1a  2277  ceqsalg  2800  cgsexg  2807  cgsex2g  2808  cgsex4g  2809  ceqsex  2810  spc2egv  2863  spc3egv  2865  csbiebt  3133  dfiin2g  3960  sotricim  4370  ralxfrALT  4514  iunpw  4527  opelxp  4705  ssrel  4763  ssrel2  4765  ssrelrel  4775  iss  5005  funcnvuni  5343  fun11iun  5543  tfrlem8  6404  eroveu  6713  fundmen  6898  nneneq  6954  fidifsnen  6967  prarloclem5  7613  prarloc  7616  recexprlemss1l  7748  recexprlemss1u  7749  uzin  9681  indstr  9714  elfzmlbp  10254  swrdnd  11112