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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimparc  299  pm5.32  457  oplem1  988  ax11i  1766  equsex  1780  eleq1a  2310  ceqsalg  2850  cgsexg  2857  cgsex2g  2858  cgsex4g  2859  ceqsex  2860  spc2egv  2915  spc3egv  2917  csbiebt  3187  dfiin2g  4045  sotricim  4468  ralxfrALT  4613  iunpw  4626  opelxp  4804  ssrel  4863  ssrel2  4865  ssrelrel  4875  iss  5109  funcnvuni  5450  fun11iun  5660  tfrlem8  6589  eroveu  6900  fundmen  7094  nneneq  7158  fidifsnen  7172  prarloclem5  7867  prarloc  7870  recexprlemss1l  8002  recexprlemss1u  8003  uzin  9955  indstr  9993  elfzmlbp  10539  swrdnd  11431  isclwwlknx  16657