Theorem con4 113

Description: Alias for ax-3 8 to be used instead of it for labeling consistency. Its associated inference is con4i 114 and its associated deduction is con4d 115. (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  114  con4d  115  con34b  315  meredith  1645  bj-alcomexcom  34789  frege54cor0a  41360  notnotrALTVD  42424  con3ALTVD  42425