Metamath Proof Explorer


Theorem con3ALT

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.)

Ref Expression
Assertion con3ALT φψ¬ψ¬φ

Proof

Step Hyp Ref Expression
1 id if-φψψφψif-φψψφψ
2 1 notbid if-φψψφψ¬if-φψψφ¬ψ
3 2 imbi1d if-φψψφψ¬if-φψψφ¬φ¬ψ¬φ
4 imbi2 if-φψψφψφif-φψψφφψ
5 imbi2 if-φψψφφφif-φψψφφφ
6 id φφ
7 4 5 6 elimh φif-φψψφ
8 7 con3i ¬if-φψψφ¬φ
9 3 8 dedt φψ¬ψ¬φ