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

Step	Hyp	Ref	Expression
1		nfnae 2058	. . . . . 6
2		nfnae 2058	. . . . . 6
3	1, 2	nfan 1928	. . . . 5
4		nfnae 2058	. . . . . . 7
5		nfnae 2058	. . . . . . 7
6	4, 5	nfan 1928	. . . . . 6
7		axc9 2046	. . . . . . 7
8	7	imp 429	. . . . . 6
9	6, 8	alrimi 1877	. . . . 5
10	3, 9	alrimi 1877	. . . 4
11	10	ex 434	. . 3
12	11	orrd 378	. 2
13	12	orri 376	1

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