Theorem con4biddc 753

Description: A contraposition deduction. (Contributed by Jim Kingdon, 18-May-2018.)

Hypothesis

Ref	Expression
con4biddc.1	⊢ (φ → (DECID ψ → (DECID χ → (¬ ψ ↔ ¬ χ))))

Assertion

Ref	Expression
con4biddc	⊢ (φ → (DECID ψ → (DECID χ → (ψ ↔ χ))))

Proof of Theorem con4biddc

Step	Hyp	Ref	Expression
1		con4biddc.1	. . . . . 6 ⊢ (φ → (DECID ψ → (DECID χ → (¬ ψ ↔ ¬ χ))))
2		bi2 121	. . . . . 6 ⊢ ((¬ ψ ↔ ¬ χ) → (¬ χ → ¬ ψ))
3	1, 2	syl8 65	. . . . 5 ⊢ (φ → (DECID ψ → (DECID χ → (¬ χ → ¬ ψ))))
4		condc 748	. . . . . 6 ⊢ (DECID χ → ((¬ χ → ¬ ψ) → (ψ → χ)))
5	4	a2i 11	. . . . 5 ⊢ ((DECID χ → (¬ χ → ¬ ψ)) → (DECID χ → (ψ → χ)))
6	3, 5	syl6 29	. . . 4 ⊢ (φ → (DECID ψ → (DECID χ → (ψ → χ))))
7	6	imp31 243	. . 3 ⊢ (((φ ∧ DECID ψ) ∧ DECID χ) → (ψ → χ))
8		bi1 111	. . . . . 6 ⊢ ((¬ ψ ↔ ¬ χ) → (¬ ψ → ¬ χ))
9	1, 8	syl8 65	. . . . 5 ⊢ (φ → (DECID ψ → (DECID χ → (¬ ψ → ¬ χ))))
10		condc 748	. . . . . 6 ⊢ (DECID ψ → ((¬ ψ → ¬ χ) → (χ → ψ)))
11	10	imim2d 48	. . . . 5 ⊢ (DECID ψ → ((DECID χ → (¬ ψ → ¬ χ)) → (DECID χ → (χ → ψ))))
12	9, 11	sylcom 25	. . . 4 ⊢ (φ → (DECID ψ → (DECID χ → (χ → ψ))))
13	12	imp31 243	. . 3 ⊢ (((φ ∧ DECID ψ) ∧ DECID χ) → (χ → ψ))
14	7, 13	impbid 120	. 2 ⊢ (((φ ∧ DECID ψ) ∧ DECID χ) → (ψ ↔ χ))
15	14	exp31 346	1 ⊢ (φ → (DECID ψ → (DECID χ → (ψ ↔ χ))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98  DECID wdc 741

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in2 545  ax-io 629

This theorem depends on definitions:  df-bi 110  df-dc 742

This theorem is referenced by:  necon4abiddc  2272