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  983  ax11i  1762  equsex  1776  eleq1a  2303  ceqsalg  2831  cgsexg  2838  cgsex2g  2839  cgsex4g  2840  ceqsex  2841  spc2egv  2896  spc3egv  2898  csbiebt  3167  dfiin2g  4003  sotricim  4420  ralxfrALT  4564  iunpw  4577  opelxp  4755  ssrel  4814  ssrel2  4816  ssrelrel  4826  iss  5059  funcnvuni  5399  fun11iun  5604  tfrlem8  6483  eroveu  6794  fundmen  6980  nneneq  7042  fidifsnen  7056  prarloclem5  7719  prarloc  7722  recexprlemss1l  7854  recexprlemss1u  7855  uzin  9788  indstr  9826  elfzmlbp  10366  swrdnd  11239  isclwwlknx  16266