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

Theorem con1bid 357
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 224 . . 3 (𝜑 → (𝜒 ↔ ¬ 𝜓))
32con2bid 356 . 2 (𝜑 → (𝜓 ↔ ¬ 𝜒))
43bicomd 224 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:  pm5.18  383  necon1bbid  3052  r19.9rzv  4441  onmindif  6273  iotanul  6326  ondif2  8116  cnpart  14587  sadadd2lem2  15787  isnirred  19379  isreg2  21913  kqcldsat  22269  trufil  22446  itg2cnlem2  24290  issqf  25640  eupth2lem3lem4  27937  pjnorm2  29431  atdmd  30102  atmd2  30104  dfrdg4  33309  dalawlem13  36899  infordmin  39777
  Copyright terms: Public domain W3C validator