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

Theorem con2b 363
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 212 1 ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209
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 210
This theorem is referenced by:  mt2bi  367  pm4.15  831  nancom  1487  nic-ax  1675  nic-axALT  1676  alimex  1832  dfdif3  4077  ssconb  4100  disjsn  4632  oneqmini  6231  kmlem4  9579  isprm3  16027  bnj1171  32357  bnj1176  32362  bnj1204  32369  bnj1388  32390  bnj1523  32428  fvineqsneq  34801  dfxor5  40412  pm13.196a  41066
  Copyright terms: Public domain W3C validator