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

Theorem con4 111
Description: Alias for ax-3 8 to be used instead of it for labeling consistency. Its associated inference is con4i 112 and its associated deduction is con4d 113. (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  112  con4d  113  con34b  305  meredith  1557  bj-con4iALT  31717  bj-alcomexcom  31857  frege54cor0a  37177  notnotrALTVD  38173  con3ALTVD  38174
  Copyright terms: Public domain W3C validator