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  4426  prel12g  4824  ordssun  6424  tpres  7157  fvf1pr  7264  frxp  8082  frxp2  8100  frxp3  8107  omopth2  8525  naddunif  8634  swoord1  8680  swoord2  8681  fpwwe2lem11  10570  ltapr  10974  zmulcl  12558  nn0lt2  12573  elnn1uz2  12860  mnflt  13059  mnfltpnf  13062  fzm1  13544  expeq0  14033  zzlesq  14147  swrdnnn0nd  14597  nn0o1gt2  16327  prm23lt5  16761  vdwlem9  16936  cshwshashlem1  17042  cshwshash  17051  funcres2c  17845  tsrlemax  18527  odlem1  19449  gexlem1  19493  nrhmzr  20457  0top  22903  cmpfi  23328  alexsubALTlem3  23969  dyadmbl  25534  plydivex  26238  scvxcvx  26929  gausslemma2dlem0f  27305  nb3grprlem1  29360  1to3vfriswmgr  30259  frgrwopreg  30302  frgrregorufr  30304  frgrregord13  30375  disjunsn  32573  dfon2lem4  35767  dfrdg4  35932  broutsideof2  36103  lineunray  36128  fwddifnp1  36146  meran1  36392  bj-orim2  36537  bj-peircecurry  36539  bj-falor2  36566  bj-sbsb  36818  bj-unrab  36907  wl-orel12  37492  tsor3  38136  paddclN  39829  lcfl6  41487  sbor2  42193  fsuppind  42571  omcl3g  43316  ifpid3g  43474  ifpim4  43480  rp-fakeanorass  43495  sqrtcval  43623  iunrelexp0  43684  clsk1indlem3  44025  19.33-2  44364  ax6e2ndeq  44542  undif3VD  44864  ax6e2ndeqVD  44891  ax6e2ndeqALT  44913  stoweidlem26  46017  stoweidlem37  46028  fourierswlem  46221  fouriersw  46222  elaa2lem  46224  salexct  46325  sge0z  46366  nfunsnafv2  47219  prproropf1olem4  47500  sfprmdvdsmersenne  47597  nn0o1gt2ALTV  47688  odd2prm2  47712  even3prm2  47713  stgoldbwt  47770  clnbgrel  47822  gpg5nbgrvtx03starlem1  48052  gpg5nbgrvtx03starlem2  48053  gpg5nbgrvtx03starlem3  48054  gpg5nbgrvtx13starlem1  48055  gpg5nbgrvtx13starlem2  48056  gpg5nbgrvtx13starlem3  48057  reorelicc  48692  rrx2plord2  48704  line2y  48737  opth2neg  48808