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  1617  19.33  1884  19.33b  1885  dfsb2  2498  mooran2  2556  undif4  4467  prel12g  4864  ordssun  6486  tpres  7221  fvf1pr  7327  frxp  8151  frxp2  8169  frxp3  8176  omopth2  8622  naddunif  8731  swoord1  8777  swoord2  8778  fpwwe2lem11  10681  ltapr  11085  zmulcl  12666  nn0lt2  12681  elnn1uz2  12967  mnflt  13165  mnfltpnf  13168  fzm1  13647  expeq0  14133  zzlesq  14245  swrdnnn0nd  14694  nn0o1gt2  16418  prm23lt5  16852  vdwlem9  17027  cshwshashlem1  17133  cshwshash  17142  funcres2c  17948  tsrlemax  18631  odlem1  19553  gexlem1  19597  nrhmzr  20537  0top  22990  cmpfi  23416  alexsubALTlem3  24057  dyadmbl  25635  plydivex  26339  scvxcvx  27029  gausslemma2dlem0f  27405  nb3grprlem1  29397  1to3vfriswmgr  30299  frgrwopreg  30342  frgrregorufr  30344  frgrregord13  30415  disjunsn  32607  dfon2lem4  35787  dfrdg4  35952  broutsideof2  36123  lineunray  36148  fwddifnp1  36166  meran1  36412  bj-orim2  36557  bj-peircecurry  36559  bj-falor2  36586  bj-sbsb  36838  bj-unrab  36927  wl-orel12  37512  tsor3  38156  paddclN  39844  lcfl6  41502  sbor2  42251  fsuppind  42600  omcl3g  43347  ifpid3g  43505  ifpim4  43511  rp-fakeanorass  43526  sqrtcval  43654  iunrelexp0  43715  clsk1indlem3  44056  19.33-2  44401  ax6e2ndeq  44579  undif3VD  44902  ax6e2ndeqVD  44929  ax6e2ndeqALT  44951  stoweidlem26  46041  stoweidlem37  46052  fourierswlem  46245  fouriersw  46246  elaa2lem  46248  salexct  46349  sge0z  46390  nfunsnafv2  47237  prproropf1olem4  47493  sfprmdvdsmersenne  47590  nn0o1gt2ALTV  47681  odd2prm2  47705  even3prm2  47706  stgoldbwt  47763  clnbgrel  47815  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  reorelicc  48631  rrx2plord2  48643  line2y  48676  opth2neg  48740