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

Theorem con1bid 344
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 213 . . 3 (𝜑 → (𝜒 ↔ ¬ 𝜓))
32con2bid 343 . 2 (𝜑 → (𝜓 ↔ ¬ 𝜒))
43bicomd 213 1 (𝜑 → (¬ 𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196
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 197
This theorem is referenced by:  pm5.18  370  necon1bbid  2862  r19.9rzv  4098  onmindif  5853  iotanul  5904  ondif2  7627  cnpart  14024  sadadd2lem2  15219  isnirred  18746  isreg2  21229  kqcldsat  21584  trufil  21761  itg2cnlem2  23574  issqf  24907  eupth2lem3lem4  27209  pjnorm2  28714  atdmd  29385  atmd2  29387  dfrdg4  32183  dalawlem13  35487
  Copyright terms: Public domain W3C validator