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  2497  mooran2  2555  undif4  4442  prel12g  4840  ordssun  6456  tpres  7193  fvf1pr  7300  frxp  8125  frxp2  8143  frxp3  8150  omopth2  8596  naddunif  8705  swoord1  8751  swoord2  8752  fpwwe2lem11  10655  ltapr  11059  zmulcl  12641  nn0lt2  12656  elnn1uz2  12941  mnflt  13139  mnfltpnf  13142  fzm1  13624  expeq0  14110  zzlesq  14224  swrdnnn0nd  14674  nn0o1gt2  16400  prm23lt5  16834  vdwlem9  17009  cshwshashlem1  17115  cshwshash  17124  funcres2c  17916  tsrlemax  18596  odlem1  19516  gexlem1  19560  nrhmzr  20497  0top  22921  cmpfi  23346  alexsubALTlem3  23987  dyadmbl  25553  plydivex  26257  scvxcvx  26948  gausslemma2dlem0f  27324  nb3grprlem1  29359  1to3vfriswmgr  30261  frgrwopreg  30304  frgrregorufr  30306  frgrregord13  30377  disjunsn  32575  dfon2lem4  35804  dfrdg4  35969  broutsideof2  36140  lineunray  36165  fwddifnp1  36183  meran1  36429  bj-orim2  36574  bj-peircecurry  36576  bj-falor2  36603  bj-sbsb  36855  bj-unrab  36944  wl-orel12  37529  tsor3  38173  paddclN  39861  lcfl6  41519  sbor2  42263  fsuppind  42613  omcl3g  43358  ifpid3g  43516  ifpim4  43522  rp-fakeanorass  43537  sqrtcval  43665  iunrelexp0  43726  clsk1indlem3  44067  19.33-2  44406  ax6e2ndeq  44584  undif3VD  44906  ax6e2ndeqVD  44933  ax6e2ndeqALT  44955  stoweidlem26  46055  stoweidlem37  46066  fourierswlem  46259  fouriersw  46260  elaa2lem  46262  salexct  46363  sge0z  46404  nfunsnafv2  47254  prproropf1olem4  47520  sfprmdvdsmersenne  47617  nn0o1gt2ALTV  47708  odd2prm2  47732  even3prm2  47733  stgoldbwt  47790  clnbgrel  47842  gpg5nbgrvtx03starlem1  48070  gpg5nbgrvtx03starlem2  48071  gpg5nbgrvtx03starlem3  48072  gpg5nbgrvtx13starlem1  48073  gpg5nbgrvtx13starlem2  48074  gpg5nbgrvtx13starlem3  48075  reorelicc  48690  rrx2plord2  48702  line2y  48735  opth2neg  48805