Theorem olc 384

Description: Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.)

Assertion

Ref	Expression
olc

Proof of Theorem olc

Step	Hyp	Ref	Expression
1		ax-1 6	. 2
2	1	orrd 378	1

Syntax hints:  -.wn 3  ->wi 4  \/wo 368

This theorem is referenced by:  pm1.4  386  pm2.07  396  pm2.46  398  biorf  405  pm1.5  522  pm2.41  573  jaob  783  pm3.48  833  norbi  859  andi  867  pm4.72  876  dedlemb  955  consensus  959  cad1  1465  19.33  1695  19.33b  1696  dfsb2  2114  mooran2  2349  undif3  3758  undif4  3883  ordelinel  4981  ordssun  4982  ordequn  4983  frxp  6910  omopth2  7252  swoord1  7359  swoord2  7360  sucprcregOLD  8047  rankxplim3  8320  fpwwe2lem12  9040  ltapr  9444  zmulcl  10937  nn0lt2  10952  elnn1uz2  11187  mnflt  11362  mnfltpnf  11364  fzm1  11787  expeq0  12196  vdwlem9  14507  cshwshashlem1  14580  cshwshash  14589  funcres2c  15270  tsrlemax  15850  odlem1  16559  gexlem1  16599  0top  19485  cmpfi  19908  alexsubALTlem3  20549  dyadmbl  22009  plydivex  22693  scvxcvx  23315  nb3graprlem1  24451  uvtx01vtx  24492  1to3vfriswmgra  25007  frgraregorufr  25053  frgraregord13  25119  disjunsn  27453  dfon2lem4  29218  sltsgn1  29421  sltsgn2  29422  dfrdg4  29600  broutsideof2  29772  lineunray  29797  meran1  29876  tsor3  30556  prtlem90  30598  19.33-2  31287  stoweidlem26  31808  stoweidlem37  31819  fourierswlem  32013  fouriersw  32014  elaa2lem  32016  tpres  32554  nrhmzr  32679  ax6e2ndeq  33332  undif3VD  33682  ax6e2ndeqVD  33709  ax6e2ndeqALT  33731  anifp  34158  bj-falor2  34174  bj-nfntht  34199  bj-nfntht2  34200  bj-unrab  34494  paddclN  35566  lcfl6  37227  bj-ifid3g  37710  rp-fakeanorass  37737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-or 370