Theorem bicon1i 193

Description: A contraposition inference.

Hypothesis

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

Assertion

Ref	Expression
bicon1i	⊢ (¬ ψ ↔ φ)

Proof of Theorem bicon1i

Step	Hyp	Ref	Expression
1		bicon1.1	. . . 4 ⊢ (¬ φ ↔ ψ)
2	1	biimp 133	. . 3 ⊢ (¬ φ → ψ)
3	2	con1i 88	. 2 ⊢ (¬ ψ → φ)
4	1	biimpr 134	. . 3 ⊢ (ψ → ¬ φ)
5	4	con2i 89	. 2 ⊢ (φ → ¬ ψ)
6	3, 5	impbi 139	1 ⊢ (¬ ψ ↔ φ)

Syntax hints:  ¬ wn 1   ↔ wb 127

This theorem is referenced by:  bicon2i 194  dfbi 499  dfnul3 1710  rab0 1718  class2set 1747  snprc 1838  opth2 1909  onxpdisj 2476  imasn 2616  intirr 2628  fvprc 2829  fvopabn 2873  ecelqsdm 3235  kmlem3 3582  axpowndlem3 3745  nnunb 4520  climunii 4883  hlimunii 5143  large 5700

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

This theorem depends on definitions:  df-bi 128

metamath.org