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	⊢ ( ( 𝜑 → 𝜓 ) → ( ¬ 𝜓 → ¬ 𝜑 ) )