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  984  ax11i  1762  equsex  1776  eleq1a  2304  ceqsalg  2842  cgsexg  2849  cgsex2g  2850  cgsex4g  2851  ceqsex  2852  spc2egv  2907  spc3egv  2909  csbiebt  3178  dfiin2g  4024  sotricim  4444  ralxfrALT  4588  iunpw  4601  opelxp  4779  ssrel  4838  ssrel2  4840  ssrelrel  4850  iss  5084  funcnvuni  5425  fun11iun  5635  tfrlem8  6549  eroveu  6860  fundmen  7047  nneneq  7111  fidifsnen  7125  prarloclem5  7815  prarloc  7818  recexprlemss1l  7950  recexprlemss1u  7951  uzin  9887  indstr  9925  elfzmlbp  10466  swrdnd  11351  isclwwlknx  16411