Theorem iddii 41708

Description: Version of a1ii 2 with the hypotheses switched. The first hypothesis is redundant so this theorem should not normally appear in a proof. Inference associated with idd 24. (Contributed by SN, 1-Apr-2025.) (New usage is discouraged.)

Hypotheses

Ref	Expression
iddii.1	⊢ 𝜑
iddii.2	⊢ 𝜓

Assertion

Ref	Expression
iddii	⊢ 𝜓

Proof of Theorem iddii

Step	Hyp	Ref	Expression
1		iddii.2	1 ⊢ 𝜓

This theorem is referenced by:  aprilfools2025  41718