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  1613  19.33  1881  19.33b  1882  dfsb2  2495  mooran2  2553  undif4  4472  prel12g  4868  ordssun  6487  tpres  7220  fvf1pr  7326  frxp  8149  frxp2  8167  frxp3  8174  omopth2  8620  naddunif  8729  swoord1  8775  swoord2  8776  fpwwe2lem11  10678  ltapr  11082  zmulcl  12663  nn0lt2  12678  elnn1uz2  12964  mnflt  13162  mnfltpnf  13165  fzm1  13643  expeq0  14129  zzlesq  14241  swrdnnn0nd  14690  nn0o1gt2  16414  prm23lt5  16847  vdwlem9  17022  cshwshashlem1  17129  cshwshash  17138  funcres2c  17954  tsrlemax  18643  odlem1  19567  gexlem1  19611  nrhmzr  20553  0top  23005  cmpfi  23431  alexsubALTlem3  24072  dyadmbl  25648  plydivex  26353  scvxcvx  27043  gausslemma2dlem0f  27419  nb3grprlem1  29411  1to3vfriswmgr  30308  frgrwopreg  30351  frgrregorufr  30353  frgrregord13  30424  disjunsn  32613  dfon2lem4  35767  dfrdg4  35932  broutsideof2  36103  lineunray  36128  fwddifnp1  36146  meran1  36393  bj-orim2  36538  bj-peircecurry  36540  bj-falor2  36567  bj-sbsb  36819  bj-unrab  36908  wl-orel12  37491  tsor3  38135  paddclN  39824  lcfl6  41482  sbor2  42229  fsuppind  42576  omcl3g  43323  ifpid3g  43481  ifpim4  43487  rp-fakeanorass  43502  sqrtcval  43630  iunrelexp0  43691  clsk1indlem3  44032  19.33-2  44377  ax6e2ndeq  44556  undif3VD  44879  ax6e2ndeqVD  44906  ax6e2ndeqALT  44928  stoweidlem26  45981  stoweidlem37  45992  fourierswlem  46185  fouriersw  46186  elaa2lem  46188  salexct  46289  sge0z  46330  nfunsnafv2  47174  prproropf1olem4  47430  sfprmdvdsmersenne  47527  nn0o1gt2ALTV  47618  odd2prm2  47642  even3prm2  47643  stgoldbwt  47700  clnbgrel  47752  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963  reorelicc  48559  rrx2plord2  48571  line2y  48604