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

Theorem con2b 361
Description: Contraposition. Bidirectional version of con2 137. (Contributed by NM, 12-Mar-1993.)
Assertion
Ref Expression
con2b ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑))

Proof of Theorem con2b
StepHypRef Expression
1 con2 137 . 2 ((𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑))
2 con2 137 . 2 ((𝜓 → ¬ 𝜑) → (𝜑 → ¬ 𝜓))
31, 2impbii 210 1 ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 208
This theorem is referenced by:  mt2bi  365  pm4.15  828  nancom  1480  nic-ax  1665  nic-axALT  1666  alimex  1822  dfdif3  4088  ssconb  4111  disjsn  4639  oneqmini  6235  kmlem4  9567  isprm3  16015  bnj1171  32169  bnj1176  32174  bnj1204  32181  bnj1388  32202  bnj1523  32240  fvineqsneq  34575  dfxor5  39990  pm13.196a  40623
  Copyright terms: Public domain W3C validator