Theorem olc 874

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 869	1 ⊢ (𝜑 → (𝜓 ∨ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  pm1.4  875  pm2.46  888  norbi  892  pm2.07  908  pm2.41  913  pm1.5  925  biorf  942  pm4.72  957  jaob  969  pm3.48  971  andi  1015  dedlemb  1052  consensus  1058  anifp  1077  cad1  1624  19.33  1891  19.33b  1892  dfsb2  2501  mooran2  2560  undif4  4396  prel12g  4796  ordssun  6415  tpres  7146  fvf1pr  7252  frxp  8067  frxp2  8085  frxp3  8092  omopth2  8510  naddunif  8620  swoord1  8667  swoord2  8668  fpwwe2lem11  10556  ltapr  10960  zmulcl  12568  nn0lt2  12584  elnn1uz2  12867  mnflt  13066  mnfltpnf  13069  fzm1  13553  expeq0  14046  zzlesq  14160  swrdnnn0nd  14611  nn0o1gt2  16342  prm23lt5  16777  vdwlem9  16952  cshwshashlem1  17058  cshwshash  17067  funcres2c  17862  tsrlemax  18544  odlem1  19502  gexlem1  19546  nrhmzr  20510  0top  22967  cmpfi  23392  alexsubALTlem3  24033  dyadmbl  25586  plydivex  26282  scvxcvx  26968  gausslemma2dlem0f  27343  nb3grprlem1  29468  1to3vfriswmgr  30369  frgrwopreg  30412  frgrregorufr  30414  frgrregord13  30485  disjunsn  32684  axprALT2  35299  dfon2lem4  36021  dfrdg4  36188  broutsideof2  36359  lineunray  36384  fwddifnp1  36402  meran1  36648  axtco1from2  36712  bj-orim2  36875  bj-peircecurry  36877  bj-falor2  36905  bj-sbsb  37199  bj-unrab  37288  wl-orel12  37891  tsor3  38525  paddclN  40343  lcfl6  42001  sbor2  42706  fsuppind  43049  omcl3g  43788  ifpid3g  43945  ifpim4  43951  rp-fakeanorass  43966  sqrtcval  44094  iunrelexp0  44155  clsk1indlem3  44496  19.33-2  44835  ax6e2ndeq  45012  undif3VD  45334  ax6e2ndeqVD  45361  ax6e2ndeqALT  45383  stoweidlem26  46477  stoweidlem37  46488  fourierswlem  46681  fouriersw  46682  elaa2lem  46684  salexct  46785  sge0z  46826  nfunsnafv2  47696  prproropf1olem4  47989  sfprmdvdsmersenne  48089  nn0o1gt2ALTV  48193  odd2prm2  48217  even3prm2  48218  stgoldbwt  48275  clnbgrel  48327  gpg5nbgrvtx03starlem1  48567  gpg5nbgrvtx03starlem2  48568  gpg5nbgrvtx03starlem3  48569  gpg5nbgrvtx13starlem1  48570  gpg5nbgrvtx13starlem2  48571  gpg5nbgrvtx13starlem3  48572  gpg5edgnedg  48629  reorelicc  49209  rrx2plord2  49221  line2y  49254  opth2neg  49325