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  2492  mooran2  2550  undif4  4433  prel12g  4831  ordssun  6439  tpres  7178  fvf1pr  7285  frxp  8108  frxp2  8126  frxp3  8133  omopth2  8551  naddunif  8660  swoord1  8706  swoord2  8707  fpwwe2lem11  10601  ltapr  11005  zmulcl  12589  nn0lt2  12604  elnn1uz2  12891  mnflt  13090  mnfltpnf  13093  fzm1  13575  expeq0  14064  zzlesq  14178  swrdnnn0nd  14628  nn0o1gt2  16358  prm23lt5  16792  vdwlem9  16967  cshwshashlem1  17073  cshwshash  17082  funcres2c  17872  tsrlemax  18552  odlem1  19472  gexlem1  19516  nrhmzr  20453  0top  22877  cmpfi  23302  alexsubALTlem3  23943  dyadmbl  25508  plydivex  26212  scvxcvx  26903  gausslemma2dlem0f  27279  nb3grprlem1  29314  1to3vfriswmgr  30216  frgrwopreg  30259  frgrregorufr  30261  frgrregord13  30332  disjunsn  32530  dfon2lem4  35781  dfrdg4  35946  broutsideof2  36117  lineunray  36142  fwddifnp1  36160  meran1  36406  bj-orim2  36551  bj-peircecurry  36553  bj-falor2  36580  bj-sbsb  36832  bj-unrab  36921  wl-orel12  37506  tsor3  38150  paddclN  39843  lcfl6  41501  sbor2  42207  fsuppind  42585  omcl3g  43330  ifpid3g  43488  ifpim4  43494  rp-fakeanorass  43509  sqrtcval  43637  iunrelexp0  43698  clsk1indlem3  44039  19.33-2  44378  ax6e2ndeq  44556  undif3VD  44878  ax6e2ndeqVD  44905  ax6e2ndeqALT  44927  stoweidlem26  46031  stoweidlem37  46042  fourierswlem  46235  fouriersw  46236  elaa2lem  46238  salexct  46339  sge0z  46380  nfunsnafv2  47230  prproropf1olem4  47511  sfprmdvdsmersenne  47608  nn0o1gt2ALTV  47699  odd2prm2  47723  even3prm2  47724  stgoldbwt  47781  clnbgrel  47833  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  reorelicc  48703  rrx2plord2  48715  line2y  48748  opth2neg  48819