This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Propositional calculus Logical conjunction pm5.21nd
Description: Eliminate an antecedent implied by each side of a biconditional.
Variant of pm5.21ndd . (Contributed by NM , 20-Nov-2005) (Proof
shortened by Wolf Lammen , 4-Nov-2013)
Ref
Expression
Hypotheses
pm5.21nd.1 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜃 )
pm5.21nd.2 ⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝜃 )
pm5.21nd.3 ⊢ ( 𝜃 → ( 𝜓 ↔ 𝜒 ) )
Assertion
pm5.21nd ⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
Proof
Step
Hyp
Ref
Expression
1
pm5.21nd.1 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜃 )
2
pm5.21nd.2 ⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝜃 )
3
pm5.21nd.3 ⊢ ( 𝜃 → ( 𝜓 ↔ 𝜒 ) )
4
1
ex ⊢ ( 𝜑 → ( 𝜓 → 𝜃 ) )
5
2
ex ⊢ ( 𝜑 → ( 𝜒 → 𝜃 ) )
6
3
a1i ⊢ ( 𝜑 → ( 𝜃 → ( 𝜓 ↔ 𝜒 ) ) )
7
4 5 6
pm5.21ndd ⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )