Theorem pm5.21ndd 343

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.)

Hypotheses

Ref	Expression
pm5.21ndd.1	⊢ (φ → (χ → ψ))
pm5.21ndd.2	⊢ (φ → (θ → ψ))
pm5.21ndd.3	⊢ (φ → (ψ → (χ ↔ θ)))

Assertion

Ref	Expression
pm5.21ndd	⊢ (φ → (χ ↔ θ))

Proof of Theorem pm5.21ndd

Step	Hyp	Ref	Expression
1		pm5.21ndd.3	. 2 ⊢ (φ → (ψ → (χ ↔ θ)))
2		pm5.21ndd.1	. . . 4 ⊢ (φ → (χ → ψ))
3	2	con3d 125	. . 3 ⊢ (φ → (¬ ψ → ¬ χ))
4		pm5.21ndd.2	. . . 4 ⊢ (φ → (θ → ψ))
5	4	con3d 125	. . 3 ⊢ (φ → (¬ ψ → ¬ θ))
6		pm5.21im 338	. . 3 ⊢ (¬ χ → (¬ θ → (χ ↔ θ)))
7	3, 5, 6	syl6c 60	. 2 ⊢ (φ → (¬ ψ → (χ ↔ θ)))
8	1, 7	pm2.61d 150	1 ⊢ (φ → (χ ↔ θ))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 176

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 177

This theorem is used by:  pm5.21nd  868  rmob  3135  eqpw1uni  4331  fnasrn  5418  funiunfv  5468  eqncg  6127  eqtc  6162  elce  6176