This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pm5.21ndd

Description: Eliminate an antecedent implied by each side of a biconditional, deduction version. (Contributed by Paul Chapman, 21-Nov-2012) (Proof shortened by Wolf Lammen, 6-Oct-2013)

	Ref	Expression
Hypotheses	pm5.21ndd.1	$⊢ φ \to (χ \to ψ)$
	pm5.21ndd.2	$⊢ φ \to (θ \to ψ)$
	pm5.21ndd.3	$⊢ φ \to (ψ \to (χ \leftrightarrow θ))$
Assertion	pm5.21ndd	$⊢ φ \to (χ \leftrightarrow θ)$

Proof

Step	Hyp	Ref	Expression
1		pm5.21ndd.1	$⊢ φ \to (χ \to ψ)$
2		pm5.21ndd.2	$⊢ φ \to (θ \to ψ)$
3		pm5.21ndd.3	$⊢ φ \to (ψ \to (χ \leftrightarrow θ))$
4	1	con3d	$⊢ φ \to (\neg ψ \to \neg χ)$
5	2	con3d	$⊢ φ \to (\neg ψ \to \neg θ)$
6		pm5.21im	$⊢ \neg χ \to (\neg θ \to (χ \leftrightarrow θ))$
7	4 5 6	syl6c	$⊢ φ \to (\neg ψ \to (χ \leftrightarrow θ))$
8	3 7	pm2.61d	$⊢ φ \to (χ \leftrightarrow θ)$