Theorem olc 879

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

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

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 859

This theorem is referenced by:  pm1.4  880  pm2.46  893  norbi  897  pm2.07  913  pm2.41  918  pm1.5  930  biorf  947  pm4.72  962  jaob  974  pm3.48  976  andi  1021  dedlemb  1058  consensus  1064  anifp  1084  cad1  1639  19.33  1906  19.33b  1907  dfsb2  2526  mooran2  2585  undif4  4423  prel12g  4824  ordssun  6452  tpres  7187  fvf1pr  7293  frxp  8108  frxp2  8126  frxp3  8133  omopth2  8555  naddunif  8666  swoord1  8713  swoord2  8714  fpwwe2lem11  10601  ltapr  11005  zmulcl  12622  nn0lt2  12638  elnn1uz2  12928  mnflt  13127  mnfltpnf  13130  fzm1  13614  expeq0  14107  zzlesq  14221  swrdnnn0nd  14672  nn0o1gt2  16417  prm23lt5  16852  vdwlem9  17027  cshwshashlem1  17133  cshwshash  17142  funcres2c  17938  tsrlemax  18620  odlem1  19577  gexlem1  19621  nrhmzr  20589  0top  23045  cmpfi  23470  alexsubALTlem3  24111  dyadmbl  25664  plydivex  26363  scvxcvx  27052  gausslemma2dlem0f  27427  nb3grprlem1  29583  1to3vfriswmgr  30484  frgrwopreg  30527  frgrregorufr  30529  frgrregord13  30600  disjunsn  32796  axprALT2  35409  dfon2lem4  36139  dfrdg4  36306  broutsideof2  36477  lineunray  36502  fwddifnp1  36520  meran1  36776  axtco1from2  36840  bj-orim2  37003  bj-peircecurry  37005  bj-falor2  37033  bj-sbsb  37327  bj-unrab  37416  wl-orel12  38019  tsor3  38653  paddclN  40471  lcfl6  42129  sbor2  42834  fsuppind  43177  omcl3g  43916  ifpid3g  44073  ifpim4  44079  rp-fakeanorass  44094  sqrtcval  44222  iunrelexp0  44283  clsk1indlem3  44624  19.33-2  44963  ax6e2ndeq  45140  undif3VD  45462  ax6e2ndeqVD  45489  ax6e2ndeqALT  45511  stoweidlem26  46605  stoweidlem37  46616  fourierswlem  46809  fouriersw  46810  elaa2lem  46812  salexct  46913  sge0z  46954  nfunsnafv2  47824  prproropf1olem4  48117  sfprmdvdsmersenne  48217  nn0o1gt2ALTV  48321  odd2prm2  48345  even3prm2  48346  stgoldbwt  48403  clnbgrel  48455  gpg5nbgrvtx03starlem1  48695  gpg5nbgrvtx03starlem2  48696  gpg5nbgrvtx03starlem3  48697  gpg5nbgrvtx13starlem1  48698  gpg5nbgrvtx13starlem2  48699  gpg5nbgrvtx13starlem3  48700  gpg5edgnedg  48757  reorelicc  49337  rrx2plord2  49349  line2y  49382  opth2neg  49453