MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con4 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 ax-3 8 1 ((¬ 𝜑 → ¬ 𝜓) → (𝜓𝜑))
Colors of variables: wff setvar class
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  319  meredith  1643  bj-alcomexcom  34088  frege54cor0a  40495  notnotrALTVD  41555  con3ALTVD  41556
  Copyright terms: Public domain W3C validator