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

Theorem con4 110
Description: Alias for ax-3 8 to be used instead of it for labeling consistency. Its associated inference is con4i 111 and its associated deduction is con4d 112. (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  111  con4d  112  con34b  304  meredith  1556  bj-con4iALT  31552  bj-alcomexcom  31692  frege54cor0a  37074  notnotrALTVD  38070  con3ALTVD  38071
  Copyright terms: Public domain W3C validator