Theorem con2bii 228

Description: A contraposition inference.

Hypothesis

Ref	Expression
con2bii.1	⊢ (φ ↔ ¬ ψ)

Assertion

Ref	Expression
con2bii	⊢ (ψ ↔ ¬ φ)

Proof of Theorem con2bii

Step	Hyp	Ref	Expression
1		con2bii.1	. . . 4 ⊢ (φ ↔ ¬ ψ)
2	1	bicomi 179	. . 3 ⊢ (¬ ψ ↔ φ)
3	2	con1bii 227	. 2 ⊢ (¬ φ ↔ ψ)
4	3	bicomi 179	1 ⊢ (ψ ↔ ¬ φ)

Syntax hints:  ¬ wn 2   ↔ wb 153

This theorem is referenced by:  iman 244  annim 245  imnan 249  pm4.53 315  pm4.55 317  pm5.18 670  nbbn 671  xor3 684  alnex 1044  exnal 1049  exanali 1054  19.35 1086  19.41 1106  equs3 1160  equsex 1163  nne 1603  dfral2 1669  dfrex2 1670  r19.35 1773  ddif 2187  dfun2 2261  dfin2 2262  dfnul2 2300  noel 2302  disj4 2336  onuninsuci 3131  intirr 3464  rankxplim3 4739  alephgeom 4910  reclem2pr 5185  ltnlei 5607  infdif 7618  infpss 7624  elcls 7747  avril1 8825

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 154

Copyright terms: Public domain