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  4418  prel12g  4815  ordssun  6411  tpres  7137  fvf1pr  7244  frxp  8059  frxp2  8077  frxp3  8084  omopth2  8502  naddunif  8611  swoord1  8657  swoord2  8658  fpwwe2lem11  10535  ltapr  10939  zmulcl  12524  nn0lt2  12539  elnn1uz2  12826  mnflt  13025  mnfltpnf  13028  fzm1  13510  expeq0  13999  zzlesq  14113  swrdnnn0nd  14563  nn0o1gt2  16292  prm23lt5  16726  vdwlem9  16901  cshwshashlem1  17007  cshwshash  17016  funcres2c  17810  tsrlemax  18492  odlem1  19414  gexlem1  19458  nrhmzr  20422  0top  22868  cmpfi  23293  alexsubALTlem3  23934  dyadmbl  25499  plydivex  26203  scvxcvx  26894  gausslemma2dlem0f  27270  nb3grprlem1  29329  1to3vfriswmgr  30228  frgrwopreg  30271  frgrregorufr  30273  frgrregord13  30344  disjunsn  32543  dfon2lem4  35780  dfrdg4  35945  broutsideof2  36116  lineunray  36141  fwddifnp1  36159  meran1  36405  bj-orim2  36550  bj-peircecurry  36552  bj-falor2  36579  bj-sbsb  36831  bj-unrab  36920  wl-orel12  37505  tsor3  38149  paddclN  39841  lcfl6  41499  sbor2  42205  fsuppind  42583  omcl3g  43327  ifpid3g  43485  ifpim4  43491  rp-fakeanorass  43506  sqrtcval  43634  iunrelexp0  43695  clsk1indlem3  44036  19.33-2  44375  ax6e2ndeq  44553  undif3VD  44875  ax6e2ndeqVD  44902  ax6e2ndeqALT  44924  stoweidlem26  46027  stoweidlem37  46038  fourierswlem  46231  fouriersw  46232  elaa2lem  46234  salexct  46335  sge0z  46376  nfunsnafv2  47229  prproropf1olem4  47510  sfprmdvdsmersenne  47607  nn0o1gt2ALTV  47698  odd2prm2  47722  even3prm2  47723  stgoldbwt  47780  clnbgrel  47832  gpg5nbgrvtx03starlem1  48072  gpg5nbgrvtx03starlem2  48073  gpg5nbgrvtx03starlem3  48074  gpg5nbgrvtx13starlem1  48075  gpg5nbgrvtx13starlem2  48076  gpg5nbgrvtx13starlem3  48077  gpg5edgnedg  48134  reorelicc  48715  rrx2plord2  48727  line2y  48760  opth2neg  48831