Theorem con4 114

Description: Alias for ax-3 8 to be used instead of it for labeling consistency. Its associated inference is con4i 115 and its associated deduction is con4d 116. (Contributed by BJ, 24-Dec-2020.)

Assertion

Ref	Expression
con4	⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))

Proof of Theorem con4

Step	Hyp	Ref	Expression
1		ax-3 8	1 ⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-3 8

This theorem is referenced by:  con4i  115  con4d  116  con34b  319  meredith  1664  frege54cor0a  44451  notnotrALTVD  45488  con3ALTVD  45489