Theorem pclem6 555

Description: Negation inferred from embedded conjunct.

Assertion

Ref	Expression
pclem6	⊢ ((φ ↔ (ψ ∧ ¬ φ)) → ¬ ψ)

Proof of Theorem pclem6

Step	Hyp	Ref	Expression
1		bi1 130	. . . 4 ⊢ ((φ ↔ (ψ ∧ ¬ φ)) → (φ → (ψ ∧ ¬ φ)))
2		pm3.27 260	. . . 4 ⊢ ((ψ ∧ ¬ φ) → ¬ φ)
3	1, 2	syl6 23	. . 3 ⊢ ((φ ↔ (ψ ∧ ¬ φ)) → (φ → ¬ φ))
4	3	pm2.01d 81	. 2 ⊢ ((φ ↔ (ψ ∧ ¬ φ)) → ¬ φ)
5		bi2 131	. . . . 5 ⊢ ((φ ↔ (ψ ∧ ¬ φ)) → ((ψ ∧ ¬ φ) → φ))
6	5	exp3a 292	. . . 4 ⊢ ((φ ↔ (ψ ∧ ¬ φ)) → (ψ → (¬ φ → φ)))
7	6	com23 32	. . 3 ⊢ ((φ ↔ (ψ ∧ ¬ φ)) → (¬ φ → (ψ → φ)))
8		con3 86	. . 3 ⊢ ((ψ → φ) → (¬ φ → ¬ ψ))
9	7, 8	syli 52	. 2 ⊢ ((φ ↔ (ψ ∧ ¬ φ)) → (¬ φ → ¬ ψ))
10	4, 9	mpd 46	1 ⊢ ((φ ↔ (ψ ∧ ¬ φ)) → ¬ ψ)

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196

This theorem is referenced by:  nalset 1482

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org