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  305  meredith  1713  bj-con4iALT  32878  bj-alcomexcom  33001  frege54cor0a  38676  notnotrALTVD  39667  con3ALTVD  39668
  Copyright terms: Public domain W3C validator