Metamath Proof Explorer

Theorem consym1

Description: A symmetry with /\ .

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

		Ref	Expression
	Assertion	consym1	$⊢ (ψ \land (ψ \land ⊥)) \to (ψ \land φ)$

Step	Hyp	Ref	Expression
1		falim	$⊢ ⊥ \to ((ψ \land (ψ \land ⊥)) \to (ψ \land φ))$
2	1	ad2antll	$⊢ (ψ \land (ψ \land ⊥)) \to ((ψ \land (ψ \land ⊥)) \to (ψ \land φ))$
3	2	pm2.43i	$⊢ (ψ \land (ψ \land ⊥)) \to (ψ \land φ)$