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

Theorem con4bii 321
Description: A contraposition inference. (Contributed by NM, 21-May-1994.)
Hypothesis
Ref Expression
con4bii.1 𝜑 ↔ ¬ 𝜓)
Assertion
Ref Expression
con4bii (𝜑𝜓)

Proof of Theorem con4bii
StepHypRef Expression
1 con4bii.1 . 2 𝜑 ↔ ¬ 𝜓)
2 notbi 319 . 2 ((𝜑𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))
31, 2mpbir 230 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205
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 206
This theorem is referenced by:  2false  376  equsexvw  2009  cbvexv1  2339  cbvex2v  2341  cbvex  2398  cbvex2  2411  2ralorOLD  3221  rexcom  3274  cbvrexfw  3289  ceqsex  3493  ceqsexv  3495  gencbval  3507  ceqsralbv  3608  snnzb  4680  raldifsnb  4757  uni0b  4895  opab0  5512  tsna1  36606  ralopabb  41690
  Copyright terms: Public domain W3C validator