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  2972  r19.9rzv  4210  onmindif  5977  iotanul  6028  ondif2  7754  cnpart  14200  sadadd2lem2  15395  isnirred  18921  isreg2  21404  kqcldsat  21759  trufil  21936  itg2cnlem2  23749  issqf  25083  eupth2lem3lem4  27405  pjnorm2  28917  atdmd  29588  atmd2  29590  dfrdg4  32386  dalawlem13  35691
 Copyright terms: Public domain W3C validator