Theorem 3jcadALT

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

	Ref	Expression
Hypotheses	3jcadALT.1	|- ( ph -> ( ps -> ch ) )
	3jcadALT.2	|- ( ph -> ( ps -> th ) )
	3jcadALT.3	|- ( ph -> ( ps -> ta ) )
Assertion	3jcadALT	|- ( ph -> ( ps -> ( ch /\ th /\ ta ) ) )

Proof

Step	Hyp	Ref	Expression
1		3jcadALT.1	|- ( ph -> ( ps -> ch ) )
2		3jcadALT.2	|- ( ph -> ( ps -> th ) )
3		3jcadALT.3	|- ( ph -> ( ps -> ta ) )
4	1 2	jcad	|- ( ph -> ( ps -> ( ch /\ th ) ) )
5	4 3	jcad	|- ( ph -> ( ps -> ( ( ch /\ th ) /\ ta ) ) )
6		df-3an	|- ( ( ch /\ th /\ ta ) <-> ( ( ch /\ th ) /\ ta ) )
7	5 6	imbitrrdi	|- ( ph -> ( ps -> ( ch /\ th /\ ta ) ) )