Theorem olc 865

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

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

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 206  df-or 845

This theorem is referenced by:  pm1.4  866  pm2.46  880  norbi  884  pm2.07  900  pm2.41  905  pm1.5  917  biorf  934  pm4.72  947  jaob  959  pm3.48  961  andi  1005  dedlemb  1044  consensus  1050  anifp  1069  norassOLD  1536  cad1  1619  19.33  1887  19.33b  1888  dfsb2  2497  mooran2  2556  undif4  4400  prel12g  4794  ordssun  6365  tpres  7076  frxp  7967  omopth2  8415  swoord1  8529  swoord2  8530  fpwwe2lem11  10397  ltapr  10801  zmulcl  12369  nn0lt2  12383  elnn1uz2  12665  mnflt  12859  mnfltpnf  12862  fzm1  13336  expeq0  13813  swrdnnn0nd  14369  nn0o1gt2  16090  prm23lt5  16515  vdwlem9  16690  cshwshashlem1  16797  cshwshash  16806  funcres2c  17617  tsrlemax  18304  odlem1  19143  gexlem1  19184  0top  22133  cmpfi  22559  alexsubALTlem3  23200  dyadmbl  24764  plydivex  25457  scvxcvx  26135  gausslemma2dlem0f  26509  nb3grprlem1  27747  1to3vfriswmgr  28644  frgrwopreg  28687  frgrregorufr  28689  frgrregord13  28760  disjunsn  30933  dfon2lem4  33762  frxp2  33791  frxp3  33797  dfrdg4  34253  broutsideof2  34424  lineunray  34449  fwddifnp1  34467  meran1  34600  bj-orim2  34736  bj-peircecurry  34738  bj-falor2  34767  bj-sbsb  35020  bj-unrab  35114  wl-orel12  35670  tsor3  36307  paddclN  37856  lcfl6  39514  sbor2  40177  fsuppind  40279  ifpid3g  41099  ifpim4  41105  rp-fakeanorass  41120  sqrtcval  41249  iunrelexp0  41310  clsk1indlem3  41653  19.33-2  42000  ax6e2ndeq  42179  undif3VD  42502  ax6e2ndeqVD  42529  ax6e2ndeqALT  42551  stoweidlem26  43567  stoweidlem37  43578  fourierswlem  43771  fouriersw  43772  elaa2lem  43774  salexct  43873  sge0z  43913  nfunsnafv2  44717  prproropf1olem4  44958  sfprmdvdsmersenne  45055  nn0o1gt2ALTV  45146  odd2prm2  45170  even3prm2  45171  stgoldbwt  45228  nrhmzr  45431  reorelicc  46056  rrx2plord2  46068  line2y  46101