Theorem olc 867

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

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

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 847

This theorem is referenced by:  pm1.4  868  pm2.46  881  norbi  885  pm2.07  901  pm2.41  906  pm1.5  918  biorf  935  pm4.72  950  jaob  962  pm3.48  964  andi  1008  dedlemb  1047  consensus  1053  anifp  1072  cad1  1614  19.33  1883  19.33b  1884  dfsb2  2501  mooran2  2559  undif4  4490  prel12g  4888  ordssun  6497  tpres  7238  fvf1pr  7343  frxp  8167  frxp2  8185  frxp3  8192  omopth2  8640  naddunif  8749  swoord1  8795  swoord2  8796  fpwwe2lem11  10710  ltapr  11114  zmulcl  12692  nn0lt2  12706  elnn1uz2  12990  mnflt  13186  mnfltpnf  13189  fzm1  13664  expeq0  14143  zzlesq  14255  swrdnnn0nd  14704  nn0o1gt2  16429  prm23lt5  16861  vdwlem9  17036  cshwshashlem1  17143  cshwshash  17152  funcres2c  17968  tsrlemax  18656  odlem1  19577  gexlem1  19621  nrhmzr  20563  0top  23011  cmpfi  23437  alexsubALTlem3  24078  dyadmbl  25654  plydivex  26357  scvxcvx  27047  gausslemma2dlem0f  27423  nb3grprlem1  29415  1to3vfriswmgr  30312  frgrwopreg  30355  frgrregorufr  30357  frgrregord13  30428  disjunsn  32616  dfon2lem4  35750  dfrdg4  35915  broutsideof2  36086  lineunray  36111  fwddifnp1  36129  meran1  36377  bj-orim2  36522  bj-peircecurry  36524  bj-falor2  36551  bj-sbsb  36803  bj-unrab  36892  wl-orel12  37465  tsor3  38109  paddclN  39799  lcfl6  41457  sbor2  42205  fsuppind  42545  omcl3g  43296  ifpid3g  43454  ifpim4  43460  rp-fakeanorass  43475  sqrtcval  43603  iunrelexp0  43664  clsk1indlem3  44005  19.33-2  44351  ax6e2ndeq  44530  undif3VD  44853  ax6e2ndeqVD  44880  ax6e2ndeqALT  44902  stoweidlem26  45947  stoweidlem37  45958  fourierswlem  46151  fouriersw  46152  elaa2lem  46154  salexct  46255  sge0z  46296  nfunsnafv2  47140  prproropf1olem4  47380  sfprmdvdsmersenne  47477  nn0o1gt2ALTV  47568  odd2prm2  47592  even3prm2  47593  stgoldbwt  47650  clnbgrel  47701  reorelicc  48444  rrx2plord2  48456  line2y  48489