Theorem biimprcd 216

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 213	1 ⊢ (χ → (φ → ψ))

Syntax hints:   → wi 4   ↔ wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  biimparc  473  ax11i  1647  ax11eq  2193  ax11el  2194  eleq1a  2422  ceqsalg  2883  cgsexg  2890  cgsex2g  2891  cgsex4g  2892  ceqsex  2893  spc2egv  2941  spc3egv  2943  csbiebt  3172  dfiin2g  4000  eqpw1uni  4330  sfintfin  4532  tfinnn  4534  sfinltfin  4535  funcnvuni  5161  fun11iun  5305  funsi  5520  fundmen  6043  dmfrec  6316