Theorem consym1

Description: A symmetry with /\ .

See negsym1 for more information. (Contributed by Anthony Hart, 4-Sep-2011)

	Ref	Expression
Assertion	consym1	⊢ ( ( 𝜓 ∧ ( 𝜓 ∧ ⊥ ) ) → ( 𝜓 ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		falim	⊢ ( ⊥ → ( ( 𝜓 ∧ ( 𝜓 ∧ ⊥ ) ) → ( 𝜓 ∧ 𝜑 ) ) )
2	1	ad2antll	⊢ ( ( 𝜓 ∧ ( 𝜓 ∧ ⊥ ) ) → ( ( 𝜓 ∧ ( 𝜓 ∧ ⊥ ) ) → ( 𝜓 ∧ 𝜑 ) ) )
3	2	pm2.43i	⊢ ( ( 𝜓 ∧ ( 𝜓 ∧ ⊥ ) ) → ( 𝜓 ∧ 𝜑 ) )