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

Theorem con1bid 355
Description: A contraposition deduction. (Contributed by NM, 9-Oct-1999.)
Hypothesis
Ref Expression
con1bid.1 (𝜑 → (¬ 𝜓𝜒))
Assertion
Ref Expression
con1bid (𝜑 → (¬ 𝜒𝜓))

Proof of Theorem con1bid
StepHypRef Expression
1 con1bid.1 . . . 4 (𝜑 → (¬ 𝜓𝜒))
21bicomd 223 . . 3 (𝜑 → (𝜒 ↔ ¬ 𝜓))
32con2bid 354 . 2 (𝜑 → (𝜓 ↔ ¬ 𝜒))
43bicomd 223 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:  pm5.18  381  necon1bbid  2979  r19.9rzv  4499  rexsng  4675  onmindif  6475  iotanul  6538  ondif2  8541  cnpart  15280  sadadd2lem2  16488  isnirred  20421  isreg2  23386  kqcldsat  23742  trufil  23919  itg2cnlem2  25798  issqf  27180  eupth2lem3lem4  30251  pjnorm2  31747  atdmd  32418  atmd2  32420  dfrdg4  35953  dalawlem13  39886  sticksstones1  42148  aks6d1c6lem4  42175  orddif0suc  43286  infordmin  43550
  Copyright terms: Public domain W3C validator