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 212 . . 3 (𝜑 → (𝜒 ↔ ¬ 𝜓))
32con2bid 343 . 2 (𝜑 → (𝜓 ↔ ¬ 𝜒))
43bicomd 212 1 (𝜑 → (¬ 𝜒𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195 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 196 This theorem is referenced by:  pm5.18  370  necon1bbid  2821  r19.9rzv  4017  onmindif  5732  ondif2  7469  cnpart  13828  sadadd2lem2  15010  isnirred  18523  isreg2  20991  kqcldsat  21346  trufil  21524  itg2cnlem2  23335  issqf  24662  eupath2lem3  26506  pjnorm2  27970  atdmd  28641  atmd2  28643  dfrdg4  31228  dalawlem13  34187  eupth2lem3lem4  41399
 Copyright terms: Public domain W3C validator