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  2978  r19.9rzv  4506  rexsng  4681  onmindif  6478  iotanul  6541  ondif2  8539  cnpart  15276  sadadd2lem2  16484  isnirred  20437  isreg2  23401  kqcldsat  23757  trufil  23934  itg2cnlem2  25812  issqf  27194  eupth2lem3lem4  30260  pjnorm2  31756  atdmd  32427  atmd2  32429  dfrdg4  35933  dalawlem13  39866  sticksstones1  42128  aks6d1c6lem4  42155  orddif0suc  43258  infordmin  43522
  Copyright terms: Public domain W3C validator