Theorem olc 864

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

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

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 844

This theorem is referenced by:  pm1.4  865  pm2.46  879  norbi  883  pm2.07  899  pm2.41  904  pm1.5  916  biorf  933  pm4.72  946  jaob  958  pm3.48  960  andi  1004  dedlemb  1041  consensus  1047  anifp  1065  norassOLD  1534  cad1  1617  19.33  1885  19.33b  1886  dfsb2  2532  dfsb2ALT  2591  mooran2  2640  undif4  4416  prel12g  4794  ordssun  6290  tpres  6963  frxp  7820  omopth2  8210  swoord1  8320  swoord2  8321  fpwwe2lem12  10063  ltapr  10467  zmulcl  12032  nn0lt2  12046  elnn1uz2  12326  mnflt  12519  mnfltpnf  12522  fzm1  12988  expeq0  13460  swrdnnn0nd  14018  nn0o1gt2  15732  prm23lt5  16151  vdwlem9  16325  cshwshashlem1  16429  cshwshash  16438  funcres2c  17171  tsrlemax  17830  odlem1  18663  gexlem1  18704  0top  21591  cmpfi  22016  alexsubALTlem3  22657  dyadmbl  24201  plydivex  24886  scvxcvx  25563  gausslemma2dlem0f  25937  nb3grprlem1  27162  1to3vfriswmgr  28059  frgrwopreg  28102  frgrregorufr  28104  frgrregord13  28175  disjunsn  30344  dfon2lem4  33031  dfrdg4  33412  broutsideof2  33583  lineunray  33608  fwddifnp1  33626  meran1  33759  bj-orim2  33891  bj-peircecurry  33893  bj-falor2  33919  bj-sbsb  34160  bj-unrab  34247  wl-orel12  34766  tsor3  35442  paddclN  36993  lcfl6  38651  sbor2  39123  ifpid3g  39878  ifpim4  39884  rp-fakeanorass  39899  iunrelexp0  40067  clsk1indlem3  40413  19.33-2  40734  ax6e2ndeq  40913  undif3VD  41236  ax6e2ndeqVD  41263  ax6e2ndeqALT  41285  stoweidlem26  42331  stoweidlem37  42342  fourierswlem  42535  fouriersw  42536  elaa2lem  42538  salexct  42637  sge0z  42677  nfunsnafv2  43444  prproropf1olem4  43688  sfprmdvdsmersenne  43788  nn0o1gt2ALTV  43879  odd2prm2  43903  even3prm2  43904  stgoldbwt  43961  nrhmzr  44164  reorelicc  44717  rrx2plord2  44729  line2y  44762