Theorem biigb 129

Description: This proof of bii 140, discovered by Gregory Bush on 8-Mar-04, has several curious properties. First, it has only 17 steps directly from the axioms and df-bi 128, compared to over 800 steps were the proof of bii 140 expanded into axioms. Second, step 2 demands only the property of "true"; any axiom (or theorem) could be used. Third, it illustrates how intermediate steps can "blow up" in size even in short proofs. Fourth, the compressed proof is only 2.5 lines long, but the web page is over 200kB in size. If there were an obfuscated code contest for proofs, this might be a winner.

Assertion

Ref	Expression
biigb	⊢ ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))

Proof of Theorem biigb

Step	Hyp	Ref	Expression
1		df-bi 128	. 2 ⊢ ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))
2		ax-1 3	. . 3 ⊢ (χ → (θ → χ))
3		ax-1 3	. . . . 5 ⊢ (¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → ((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))))
4		df-bi 128	. . . . . . . . 9 ⊢ ¬ ((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))))
5		ax-1 3	. . . . . . . . 9 ⊢ (¬ ((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))) → (¬ ¬ (χ → (θ → χ)) → ¬ ((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))))))
6	4, 5	ax-mp 6	. . . . . . . 8 ⊢ (¬ ¬ (χ → (θ → χ)) → ¬ ((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))))
7		ax-3 5	. . . . . . . 8 ⊢ ((¬ ¬ (χ → (θ → χ)) → ¬ ((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))))) → (((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))) → ¬ (χ → (θ → χ))))
8	6, 7	ax-mp 6	. . . . . . 7 ⊢ (((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))) → ¬ (χ → (θ → χ)))
9		ax-1 3	. . . . . . 7 ⊢ ((((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))) → ¬ (χ → (θ → χ))) → (¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → (((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))) → ¬ (χ → (θ → χ)))))
10	8, 9	ax-mp 6	. . . . . 6 ⊢ (¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → (((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))) → ¬ (χ → (θ → χ))))
11		ax-2 4	. . . . . 6 ⊢ ((¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → (((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))) → ¬ (χ → (θ → χ)))) → ((¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → ((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))))) → (¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → ¬ (χ → (θ → χ)))))
12	10, 11	ax-mp 6	. . . . 5 ⊢ ((¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → ((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))))) → (¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → ¬ (χ → (θ → χ))))
13	3, 12	ax-mp 6	. . . 4 ⊢ (¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ£/I> → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → ¬ (χ → (θ → χ)))
14		ax-3 5	. . . 4 ⊢ ((¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → ¬ (χ → (θ → χ))) → ((χ → (θ → χ)) → (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))))
15	13, 14	ax-mp 6	. . 3 ⊢ ((χ → (θ → χ)) → (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))))
16	2, 15	ax-mp 6	. 2 ⊢ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))
17	1, 16	ax-mp 6	1 ⊢ ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127

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