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  2496  mooran2  2555  undif4  4418  prel12g  4819  ordssun  6420  tpres  7147  fvf1pr  7253  frxp  8068  frxp2  8086  frxp3  8093  omopth2  8511  naddunif  8621  swoord1  8668  swoord2  8669  fpwwe2lem11  10554  ltapr  10958  zmulcl  12542  nn0lt2  12557  elnn1uz2  12840  mnflt  13039  mnfltpnf  13042  fzm1  13525  expeq0  14017  zzlesq  14131  swrdnnn0nd  14582  nn0o1gt2  16310  prm23lt5  16744  vdwlem9  16919  cshwshashlem1  17025  cshwshash  17034  funcres2c  17829  tsrlemax  18511  odlem1  19466  gexlem1  19510  nrhmzr  20472  0top  22929  cmpfi  23354  alexsubALTlem3  23995  dyadmbl  25559  plydivex  26263  scvxcvx  26954  gausslemma2dlem0f  27330  nb3grprlem1  29434  1to3vfriswmgr  30336  frgrwopreg  30379  frgrregorufr  30381  frgrregord13  30452  disjunsn  32649  dfon2lem4  35957  dfrdg4  36124  broutsideof2  36295  lineunray  36320  fwddifnp1  36338  meran1  36584  bj-orim2  36729  bj-peircecurry  36731  bj-falor2  36758  bj-sbsb  37011  bj-unrab  37100  wl-orel12  37685  tsor3  38319  paddclN  40137  lcfl6  41795  sbor2  42501  fsuppind  42870  omcl3g  43613  ifpid3g  43770  ifpim4  43776  rp-fakeanorass  43791  sqrtcval  43919  iunrelexp0  43980  clsk1indlem3  44321  19.33-2  44660  ax6e2ndeq  44837  undif3VD  45159  ax6e2ndeqVD  45186  ax6e2ndeqALT  45208  stoweidlem26  46307  stoweidlem37  46318  fourierswlem  46511  fouriersw  46512  elaa2lem  46514  salexct  46615  sge0z  46656  nfunsnafv2  47508  prproropf1olem4  47789  sfprmdvdsmersenne  47886  nn0o1gt2ALTV  47977  odd2prm2  48001  even3prm2  48002  stgoldbwt  48059  clnbgrel  48111  gpg5nbgrvtx03starlem1  48351  gpg5nbgrvtx03starlem2  48352  gpg5nbgrvtx03starlem3  48353  gpg5nbgrvtx13starlem1  48354  gpg5nbgrvtx13starlem2  48355  gpg5nbgrvtx13starlem3  48356  gpg5edgnedg  48413  reorelicc  48993  rrx2plord2  49005  line2y  49038  opth2neg  49109