Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical equivalence
pm5.21ndd
Metamath Proof Explorer
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
⊢ ( 𝜑 → ( 𝜒 → 𝜓 ) )
pm5.21ndd.2
⊢ ( 𝜑 → ( 𝜃 → 𝜓 ) )
pm5.21ndd.3
⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 ↔ 𝜃 ) ) )
Assertion
pm5.21ndd
⊢ ( 𝜑 → ( 𝜒 ↔ 𝜃 ) )
Proof
Step
Hyp
Ref
Expression
1
pm5.21ndd.1
⊢ ( 𝜑 → ( 𝜒 → 𝜓 ) )
2
pm5.21ndd.2
⊢ ( 𝜑 → ( 𝜃 → 𝜓 ) )
3
pm5.21ndd.3
⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 ↔ 𝜃 ) ) )
4
1
con3d
⊢ ( 𝜑 → ( ¬ 𝜓 → ¬ 𝜒 ) )
5
2
con3d
⊢ ( 𝜑 → ( ¬ 𝜓 → ¬ 𝜃 ) )
6
pm5.21im
⊢ ( ¬ 𝜒 → ( ¬ 𝜃 → ( 𝜒 ↔ 𝜃 ) ) )
7
4 5 6
syl6c
⊢ ( 𝜑 → ( ¬ 𝜓 → ( 𝜒 ↔ 𝜃 ) ) )
8
3 7
pm2.61d
⊢ ( 𝜑 → ( 𝜒 ↔ 𝜃 ) )