Theorem consym1

Description: A symmetry with /\ .

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

	Ref	Expression
Assertion	consym1	|- ( ( ps /\ ( ps /\ F. ) ) -> ( ps /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		falim	|- ( F. -> ( ( ps /\ ( ps /\ F. ) ) -> ( ps /\ ph ) ) )
2	1	ad2antll	|- ( ( ps /\ ( ps /\ F. ) ) -> ( ( ps /\ ( ps /\ F. ) ) -> ( ps /\ ph ) ) )
3	2	pm2.43i	|- ( ( ps /\ ( ps /\ F. ) ) -> ( ps /\ ph ) )