Theorem biimprcd 159

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

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimparc  294  pm5.32  442  oplem1  922  ax11i  1650  equsex  1664  eleq1a  2160  ceqsalg  2650  cgsexg  2657  cgsex2g  2658  cgsex4g  2659  ceqsex  2660  spc2egv  2711  spc3egv  2713  csbiebt  2970  dfiin2g  3771  sotricim  4161  ralxfrALT  4304  iunpw  4317  opelxp  4483  ssrel  4541  ssrel2  4543  ssrelrel  4553  iss  4773  funcnvuni  5098  fun11iun  5289  tfrlem8  6099  eroveu  6399  fundmen  6579  nneneq  6629  fidifsnen  6642  prarloclem5  7122  prarloc  7125  recexprlemss1l  7257  recexprlemss1u  7258  uzin  9114  indstr  9144  elfzmlbp  9606