NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  con1bii GIF version

Theorem con1bii 321
Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.)
Hypothesis
Ref Expression
con1bii.1 φψ)
Assertion
Ref Expression
con1bii ψφ)

Proof of Theorem con1bii
StepHypRef Expression
1 notnot 282 . . 3 (φ ↔ ¬ ¬ φ)
2 con1bii.1 . . 3 φψ)
31, 2xchbinx 301 . 2 (φ ↔ ¬ ψ)
43bicomi 193 1 ψφ)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 176
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 177
This theorem is referenced by:  con2bii  322  xor  861  3oran  951  had0  1403  mpto2OLD  1535  necon1abii  2567  necon1bbii  2568  npss  3379  dfnul3  3553  disj  3591  snprc  3788  dfpss4  3888  0nel1c  4159  dfnnc2  4395  eqpw1relk  4479  eqtfinrelk  4486  releqel  5807  fnfullfunlem1  5856  ovcelem1  6171  tcfnex  6244  nclennlem1  6248  nnc3n3p1  6278  nchoicelem10  6298  nchoicelem11  6299  nchoicelem16  6304  fnfreclem1  6317
  Copyright terms: Public domain W3C validator