Theorem olc 868

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 863	1 ⊢ (𝜑 → (𝜓 ∨ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  pm1.4  869  pm2.46  882  norbi  886  pm2.07  902  pm2.41  907  pm1.5  919  biorf  936  pm4.72  951  jaob  963  pm3.48  965  andi  1009  dedlemb  1046  consensus  1052  anifp  1071  cad1  1617  19.33  1884  19.33b  1885  dfsb2  2491  mooran2  2549  undif4  4430  prel12g  4828  ordssun  6436  tpres  7175  fvf1pr  7282  frxp  8105  frxp2  8123  frxp3  8130  omopth2  8548  naddunif  8657  swoord1  8703  swoord2  8704  fpwwe2lem11  10594  ltapr  10998  zmulcl  12582  nn0lt2  12597  elnn1uz2  12884  mnflt  13083  mnfltpnf  13086  fzm1  13568  expeq0  14057  zzlesq  14171  swrdnnn0nd  14621  nn0o1gt2  16351  prm23lt5  16785  vdwlem9  16960  cshwshashlem1  17066  cshwshash  17075  funcres2c  17865  tsrlemax  18545  odlem1  19465  gexlem1  19509  nrhmzr  20446  0top  22870  cmpfi  23295  alexsubALTlem3  23936  dyadmbl  25501  plydivex  26205  scvxcvx  26896  gausslemma2dlem0f  27272  nb3grprlem1  29307  1to3vfriswmgr  30209  frgrwopreg  30252  frgrregorufr  30254  frgrregord13  30325  disjunsn  32523  dfon2lem4  35774  dfrdg4  35939  broutsideof2  36110  lineunray  36135  fwddifnp1  36153  meran1  36399  bj-orim2  36544  bj-peircecurry  36546  bj-falor2  36573  bj-sbsb  36825  bj-unrab  36914  wl-orel12  37499  tsor3  38143  paddclN  39836  lcfl6  41494  sbor2  42200  fsuppind  42578  omcl3g  43323  ifpid3g  43481  ifpim4  43487  rp-fakeanorass  43502  sqrtcval  43630  iunrelexp0  43691  clsk1indlem3  44032  19.33-2  44371  ax6e2ndeq  44549  undif3VD  44871  ax6e2ndeqVD  44898  ax6e2ndeqALT  44920  stoweidlem26  46024  stoweidlem37  46035  fourierswlem  46228  fouriersw  46229  elaa2lem  46231  salexct  46332  sge0z  46373  nfunsnafv2  47226  prproropf1olem4  47507  sfprmdvdsmersenne  47604  nn0o1gt2ALTV  47695  odd2prm2  47719  even3prm2  47720  stgoldbwt  47777  clnbgrel  47829  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  reorelicc  48699  rrx2plord2  48711  line2y  48744  opth2neg  48815