Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  axbnd Unicode version

Theorem axbnd 2434
 Description: Axiom of Bundling (intuitionistic logic axiom ax-bnd). In classical logic, this and axi12 2433 are fairly straightforward consequences of axc9 2046. But in intuitionistic logic, it is not easy to add the extra A.x to axi12 2433 and so we treat the two as separate axioms. (Contributed by Jim Kingdon, 22-Mar-2018.)
Assertion
Ref Expression
axbnd

Proof of Theorem axbnd
StepHypRef Expression
1 nfnae 2058 . . . . . 6
2 nfnae 2058 . . . . . 6
31, 2nfan 1928 . . . . 5
4 nfnae 2058 . . . . . . 7
5 nfnae 2058 . . . . . . 7
64, 5nfan 1928 . . . . . 6
7 axc9 2046 . . . . . . 7
87imp 429 . . . . . 6
96, 8alrimi 1877 . . . . 5
103, 9alrimi 1877 . . . 4
1110ex 434 . . 3
1211orrd 378 . 2
1312orri 376 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4  \/wo 368  /\wa 369  A.wal 1393 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1613  df-nf 1617
 Copyright terms: Public domain W3C validator