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

Theorem con4 112
Description: Alias for ax-3 8 to be used instead of it for labeling consistency. Its associated inference is con4i 113 and its associated deduction is con4d 114. (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  113  con4d  114  con34b  306  meredith  1563  bj-con4iALT  32242  bj-alcomexcom  32365  frege54cor0a  37678  notnotrALTVD  38673  con3ALTVD  38674
  Copyright terms: Public domain W3C validator