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

Theorem con34b 319
 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 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:  mtt  368  pm4.14  806  dfbi3  1045  ifpdfbi  1066  r19.23v  3238  raldifsni  4688  dff14a  7007  weniso  7087  dfom2  7565  dfsup2  8895  wemapsolem  9001  pwfseqlem3  10074  indstr  12307  rpnnen2lem12  15573  algcvgblem  15914  isirred2  19451  isdomn2  20069  ist0-3  21960  mdegleb  24675  dchrelbas4  25837  toslublem  30690  tosglblem  30692  poimirlem25  35101  poimirlem30  35106  tsbi3  35592  isdomn3  40191  ntrneikb  40840  aacllem  45370
 Copyright terms: Public domain W3C validator