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

Theorem con34b 305
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 148 . 2 ((𝜑𝜓) → (¬ 𝜓 → ¬ 𝜑))
2 con4 111 . 2 ((¬ 𝜓 → ¬ 𝜑) → (𝜑𝜓))
31, 2impbii 198 1 ((𝜑𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195
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 196
This theorem is referenced by:  mtt  353  pm4.14  600  19.23t  2066  19.23tOLD  2206  r19.23v  3005  raldifsni  4265  dff14a  6427  weniso  6504  dfom2  6959  dfsup2  8233  wemapsolem  8338  pwfseqlem3  9361  indstr  11632  rpnnen2lem12  14793  algcvgblem  15128  isirred2  18524  isdomn2  19120  ist0-3  20959  mdegleb  23628  dchrelbas4  24768  toslublem  28998  tosglblem  29000  poimirlem25  32604  poimirlem30  32609  tsbi3  33112  isdomn3  36801  ntrneikb  37412  conss34OLD  37667  aacllem  42356
  Copyright terms: Public domain W3C validator