Theorem bicomdALT 40064

Description: Alternate proof of bicomd 226 which is shorter after expanding all parent theorems (as of 8-Aug-2024, bicom 225 depends on bicom1 224 and sylib 221 depends on syl 17). Additionally, the labels bicom1 224 and syl 17 happen to contain fewer characters than bicom 225 and sylib 221. However, neither of these conditions count as a shortening according to conventions 28640. 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 922 and pm2.31 923). 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.)

Hypothesis

Ref	Expression
bicomdALT.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
bicomdALT	⊢ (𝜑 → (𝜒 ↔ 𝜓))

Proof of Theorem bicomdALT

Step	Hyp	Ref	Expression
1		bicomdALT.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bicom1 224	. 2 ⊢ ((𝜓 ↔ 𝜒) → (𝜒 ↔ 𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜒 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209

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

This theorem depends on definitions:  df-bi 210

This theorem is referenced by: (None)