Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  axi12 Structured version   GIF version

Theorem axi12 1404
 Description: Proof that ax-i12 1395 follows from ax-bndl 1396. So that we can track which theorems rely on ax-bndl 1396, proofs should reference ax-i12 1395 rather than this theorem. (Contributed by Jim Kingdon, 17-Aug-2018.) (New usage is discouraged). (Proof modification is discouraged.)
Assertion
Ref Expression
axi12 (z z = x (z z = y z(x = yz x = y)))

Proof of Theorem axi12
StepHypRef Expression
1 ax-bndl 1396 . 2 (z z = x (z z = y xz(x = yz x = y)))
2 sp 1398 . . . 4 (xz(x = yz x = y) → z(x = yz x = y))
32orim2i 677 . . 3 ((z z = y xz(x = yz x = y)) → (z z = y z(x = yz x = y)))
43orim2i 677 . 2 ((z z = x (z z = y xz(x = yz x = y))) → (z z = x (z z = y z(x = yz x = y))))
51, 4ax-mp 7 1 (z z = x (z z = y z(x = yz x = y)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∨ wo 628  ∀wal 1240   = wceq 1242 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-bndl 1396  ax-4 1397 This theorem depends on definitions:  df-bi 110 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator