Description: Proof of con3 from its associated inference con3i that illustrates the
use of the weak deduction theorem dedt . (Contributed by NM, 27-Jun-2002) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019) Revised dedt and elimh . (Revised by Steven Nguyen, 27-Apr-2023)(Proof modification is discouraged.)(New usage is discouraged.)