Theorem olc 869

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

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

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 849

This theorem is referenced by:  pm1.4  870  pm2.46  883  norbi  887  pm2.07  903  pm2.41  908  pm1.5  920  biorf  937  pm4.72  952  jaob  964  pm3.48  966  andi  1010  dedlemb  1047  consensus  1053  anifp  1072  cad1  1619  19.33  1886  19.33b  1887  dfsb2  2498  mooran2  2557  undif4  4408  prel12g  4808  ordssun  6423  tpres  7151  fvf1pr  7257  frxp  8071  frxp2  8089  frxp3  8096  omopth2  8514  naddunif  8624  swoord1  8671  swoord2  8672  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  20509  0top  22962  cmpfi  23387  alexsubALTlem3  24028  dyadmbl  25581  plydivex  26278  scvxcvx  26967  gausslemma2dlem0f  27342  nb3grprlem1  29467  1to3vfriswmgr  30369  frgrwopreg  30412  frgrregorufr  30414  frgrregord13  30485  disjunsn  32683  axprALT2  35273  dfon2lem4  35986  dfrdg4  36153  broutsideof2  36324  lineunray  36349  fwddifnp1  36367  meran1  36613  axtco1from2  36677  bj-orim2  36840  bj-peircecurry  36842  bj-falor2  36870  bj-sbsb  37164  bj-unrab  37253  wl-orel12  37856  tsor3  38490  paddclN  40308  lcfl6  41966  sbor2  42671  fsuppind  43043  omcl3g  43786  ifpid3g  43943  ifpim4  43949  rp-fakeanorass  43964  sqrtcval  44092  iunrelexp0  44153  clsk1indlem3  44494  19.33-2  44833  ax6e2ndeq  45010  undif3VD  45332  ax6e2ndeqVD  45359  ax6e2ndeqALT  45381  stoweidlem26  46478  stoweidlem37  46489  fourierswlem  46682  fouriersw  46683  elaa2lem  46685  salexct  46786  sge0z  46827  nfunsnafv2  47691  prproropf1olem4  47984  sfprmdvdsmersenne  48084  nn0o1gt2ALTV  48188  odd2prm2  48212  even3prm2  48213  stgoldbwt  48270  clnbgrel  48322  gpg5nbgrvtx03starlem1  48562  gpg5nbgrvtx03starlem2  48563  gpg5nbgrvtx03starlem3  48564  gpg5nbgrvtx13starlem1  48565  gpg5nbgrvtx13starlem2  48566  gpg5nbgrvtx13starlem3  48567  gpg5edgnedg  48624  reorelicc  49204  rrx2plord2  49216  line2y  49249  opth2neg  49320