Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-12 Unicode version

Theorem ax-12 1393
 Description: Rederive the original version of the axiom from ax-i12 1391. Note that we need ax-4 1392 for the derivation, but the proof of ax4 1423 is nontheless non-circular since it does not use ax-12. (Contributed by Mario Carneiro, 3-Feb-2015.)
Assertion
Ref Expression
ax-12

Proof of Theorem ax-12
StepHypRef Expression
1 ax-i12 1391 . . . 4
21ori 618 . . 3
32ord 619 . 2
4 ax-4 1392 . 2
53, 4syl6 28 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wo 606  wal 1335   wceq 1383 This theorem is referenced by:  hbequidOLD  1398  a9wa9lem8  1413  a9wa9lem8OLD  1414  equidALT  1560  dvelimfALT  1585  ax17eq  1645  hbsb4  1686  sbcom  1696  dvelimALT  1800  ax11eq  1810  ax11indalem  1815  a12stdy4  1822  a12lem1  1823 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-ia1 98  ax-ia2 99  ax-ia3 100  ax-in2 528  ax-io 607  ax-i12 1391  ax-4 1392 This theorem depends on definitions:  df-bi 109
 Copyright terms: Public domain W3C validator