Theorem bicomdALT

Description: Alternate proof of bicomd which is shorter after expanding all parent theorems (as of 8-Aug-2024, bicom depends on bicom1 and sylib depends on syl ). Additionally, the labels bicom1 and syl happen to contain fewer characters than bicom and sylib . However, neither of these conditions count as a shortening according to conventions . In the first case, the criteria could easily be broken by upstream changes, and in many cases the upstream dependency tree is nontrivial (see orass and pm2.31 ). For the latter case, theorem labels are up to revision, so they are not counted in the size of a proof. (Contributed by SN, 21-May-2022) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	bicomdALT.1	|- ( ph -> ( ps <-> ch ) )
Assertion	bicomdALT	|- ( ph -> ( ch <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		bicomdALT.1	|- ( ph -> ( ps <-> ch ) )
2		bicom1	|- ( ( ps <-> ch ) -> ( ch <-> ps ) )
3	1 2	syl	|- ( ph -> ( ch <-> ps ) )