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  2303  ceqsalg  2832  cgsexg  2839  cgsex2g  2840  cgsex4g  2841  ceqsex  2842  spc2egv  2897  spc3egv  2899  csbiebt  3168  dfiin2g  4008  sotricim  4426  ralxfrALT  4570  iunpw  4583  opelxp  4761  ssrel  4820  ssrel2  4822  ssrelrel  4832  iss  5065  funcnvuni  5406  fun11iun  5613  tfrlem8  6527  eroveu  6838  fundmen  7024  nneneq  7086  fidifsnen  7100  prarloclem5  7780  prarloc  7783  recexprlemss1l  7915  recexprlemss1u  7916  uzin  9850  indstr  9888  elfzmlbp  10429  swrdnd  11306  isclwwlknx  16357