Theorem orbi2iALT

Description: Alternate proof of orbi2i . (Contributed by Hongxiu Chen, 29-Jun-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	orbi2iALT.1	|- ( ph <-> ps )
Assertion	orbi2iALT	|- ( ( ch \/ ph ) <-> ( ch \/ ps ) )

Proof

Step	Hyp	Ref	Expression
1		orbi2iALT.1	|- ( ph <-> ps )
2	1	a1i	|- ( -. ch -> ( ph <-> ps ) )
3	2	pm5.74i	|- ( ( -. ch -> ph ) <-> ( -. ch -> ps ) )
4		df-or	|- ( ( ch \/ ph ) <-> ( -. ch -> ph ) )
5		df-or	|- ( ( ch \/ ps ) <-> ( -. ch -> ps ) )
6	3 4 5	3bitr4i	|- ( ( ch \/ ph ) <-> ( ch \/ ps ) )