Theorem olc 875

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

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

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 209  df-or 855

This theorem is referenced by:  pm1.4  876  pm2.46  889  norbi  893  pm2.07  909  pm2.41  914  pm1.5  926  biorf  943  pm4.72  958  jaob  970  pm3.48  972  andi  1016  dedlemb  1053  consensus  1059  anifp  1078  cad1  1625  19.33  1892  19.33b  1893  dfsb2  2503  mooran2  2562  undif4  4398  prel12g  4798  ordssun  6418  tpres  7149  fvf1pr  7255  frxp  8070  frxp2  8088  frxp3  8095  omopth2  8513  naddunif  8623  swoord1  8670  swoord2  8671  fpwwe2lem11  10559  ltapr  10963  zmulcl  12571  nn0lt2  12587  elnn1uz2  12870  mnflt  13069  mnfltpnf  13072  fzm1  13556  expeq0  14049  zzlesq  14163  swrdnnn0nd  14614  nn0o1gt2  16345  prm23lt5  16780  vdwlem9  16955  cshwshashlem1  17061  cshwshash  17070  funcres2c  17865  tsrlemax  18547  odlem1  19505  gexlem1  19549  nrhmzr  20513  0top  22970  cmpfi  23395  alexsubALTlem3  24036  dyadmbl  25589  plydivex  26285  scvxcvx  26971  gausslemma2dlem0f  27346  nb3grprlem1  29471  1to3vfriswmgr  30372  frgrwopreg  30415  frgrregorufr  30417  frgrregord13  30488  disjunsn  32687  axprALT2  35305  dfon2lem4  36027  dfrdg4  36194  broutsideof2  36365  lineunray  36390  fwddifnp1  36408  meran1  36654  axtco1from2  36718  bj-orim2  36881  bj-peircecurry  36883  bj-falor2  36911  bj-sbsb  37205  bj-unrab  37294  wl-orel12  37897  tsor3  38531  paddclN  40349  lcfl6  42007  sbor2  42712  fsuppind  43055  omcl3g  43794  ifpid3g  43951  ifpim4  43957  rp-fakeanorass  43972  sqrtcval  44100  iunrelexp0  44161  clsk1indlem3  44502  19.33-2  44841  ax6e2ndeq  45018  undif3VD  45340  ax6e2ndeqVD  45367  ax6e2ndeqALT  45389  stoweidlem26  46483  stoweidlem37  46494  fourierswlem  46687  fouriersw  46688  elaa2lem  46690  salexct  46791  sge0z  46832  nfunsnafv2  47702  prproropf1olem4  47995  sfprmdvdsmersenne  48095  nn0o1gt2ALTV  48199  odd2prm2  48223  even3prm2  48224  stgoldbwt  48281  clnbgrel  48333  gpg5nbgrvtx03starlem1  48573  gpg5nbgrvtx03starlem2  48574  gpg5nbgrvtx03starlem3  48575  gpg5nbgrvtx13starlem1  48576  gpg5nbgrvtx13starlem2  48577  gpg5nbgrvtx13starlem3  48578  gpg5edgnedg  48635  reorelicc  49215  rrx2plord2  49227  line2y  49260  opth2neg  49331