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

Theorem con34b 317
Description: A biconditional form of contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116. (Contributed by NM, 11-May-1993.)
Assertion
Ref Expression
con34b ((𝜑𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))

Proof of Theorem con34b
StepHypRef Expression
1 con3 156 . 2 ((𝜑𝜓) → (¬ 𝜓 → ¬ 𝜑))
2 con4 113 . 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:  mtt  366  pm4.14  803  dfbi3  1041  r19.23v  3276  raldifsni  4720  dff14a  7019  weniso  7096  dfom2  7571  dfsup2  8896  wemapsolem  9002  pwfseqlem3  10070  indstr  12304  rpnnen2lem12  15566  algcvgblem  15909  isirred2  19380  isdomn2  20000  ist0-3  21881  mdegleb  24585  dchrelbas4  25746  toslublem  30581  tosglblem  30583  poimirlem25  34798  poimirlem30  34803  tsbi3  35294  isdomn3  39682  ntrneikb  40322  aacllem  44830
  Copyright terms: Public domain W3C validator