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

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

Proof of Theorem con2b
StepHypRef Expression
1 con2 135 . 2 ((𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑))
2 con2 135 . 2 ((𝜓 → ¬ 𝜑) → (𝜑 → ¬ 𝜓))
31, 2impbii 209 1 ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206
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 207
This theorem is referenced by:  mt2bi  363  pm4.15  833  nancom  1496  nic-ax  1673  nic-axALT  1674  alimex  1831  dfdif3OLD  4118  ssconb  4142  disjsn  4711  oneqmini  6436  kmlem4  10194  isprm3  16720  ssdifidlprm  33486  bnj1171  35014  bnj1176  35019  bnj1204  35026  bnj1388  35047  bnj1523  35085  fvineqsneq  37413  dfxor5  43780  pm13.196a  44433  sswfaxreg  45004
  Copyright terms: Public domain W3C validator