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	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
	3jcadALT.2	⊢ ( 𝜑 → ( 𝜓 → 𝜃 ) )
	3jcadALT.3	⊢ ( 𝜑 → ( 𝜓 → 𝜏 ) )
Assertion	3jcadALT	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 ∧ 𝜃 ∧ 𝜏 ) ) )

Proof

Step	Hyp	Ref	Expression
1		3jcadALT.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2		3jcadALT.2	⊢ ( 𝜑 → ( 𝜓 → 𝜃 ) )
3		3jcadALT.3	⊢ ( 𝜑 → ( 𝜓 → 𝜏 ) )
4	1 2	jcad	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 ∧ 𝜃 ) ) )
5	4 3	jcad	⊢ ( 𝜑 → ( 𝜓 → ( ( 𝜒 ∧ 𝜃 ) ∧ 𝜏 ) ) )
6		df-3an	⊢ ( ( 𝜒 ∧ 𝜃 ∧ 𝜏 ) ↔ ( ( 𝜒 ∧ 𝜃 ) ∧ 𝜏 ) )
7	5 6	imbitrrdi	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 ∧ 𝜃 ∧ 𝜏 ) ) )