Theorem olc 881

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

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

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 210  df-or 861

This theorem is referenced by:  pm1.4  882  pm2.46  895  norbi  899  pm2.07  915  pm2.41  920  pm1.5  932  biorf  949  pm4.72  964  jaob  976  pm3.48  978  andi  1023  dedlemb  1060  consensus  1066  anifp  1086  cad1  1645  19.33  1912  19.33b  1913  dfsb2  2532  mooran2  2591  undif4  4433  prel12g  4834  ordssun  6469  tpres  7203  fvf1pr  7309  frxp  8125  frxp2  8143  frxp3  8150  omopth2  8572  naddunif  8683  swoord1  8730  swoord2  8731  fpwwe2lem11  10629  ltapr  11033  zmulcl  12646  nn0lt2  12662  elnn1uz2  12952  mnflt  13151  mnfltpnf  13154  fzm1  13638  expeq0  14131  zzlesq  14245  swrdnnn0nd  14697  nn0o1gt2  16442  prm23lt5  16877  vdwlem9  17052  cshwshashlem1  17158  cshwshash  17167  funcres2c  17963  tsrlemax  18645  odlem1  19608  gexlem1  19652  nrhmzr  20625  0top  23123  cmpfi  23548  alexsubALTlem3  24189  dyadmbl  25742  plydivex  26441  scvxcvx  27130  gausslemma2dlem0f  27505  nb3grprlem1  29700  1to3vfriswmgr  30601  frgrwopreg  30644  frgrregorufr  30646  frgrregord13  30717  disjunsn  32909  axprALT2  35471  dfon2lem4  36234  dfrdg4  36401  broutsideof2  36572  lineunray  36597  fwddifnp1  36615  meran1  36870  axtco1from2  36934  bj-orim2  37096  bj-peircecurry  37098  bj-falor2  37126  bj-sbsb  37420  bj-unrab  37510  wl-orel12  38114  tsor3  38748  paddclN  40566  lcfl6  42224  quadfac  42922  sbor2  42931  fsuppind  43274  omcl3g  44013  ifpid3g  44170  ifpim4  44176  rp-fakeanorass  44191  sqrtcval  44319  iunrelexp0  44380  clsk1indlem3  44721  19.33-2  45044  ax6e2ndeq  45220  undif3VD  45542  ax6e2ndeqVD  45569  ax6e2ndeqALT  45591  stoweidlem26  46692  stoweidlem37  46703  fourierswlem  46896  fouriersw  46897  elaa2lem  46899  salexct  47000  sge0z  47041  nfunsnafv2  47911  prproropf1olem4  48204  sfprmdvdsmersenne  48304  nn0o1gt2ALTV  48408  odd2prm2  48432  even3prm2  48433  stgoldbwt  48490  clnbgrel  48542  gpg5nbgrvtx03starlem1  48782  gpg5nbgrvtx03starlem2  48783  gpg5nbgrvtx03starlem3  48784  gpg5nbgrvtx13starlem1  48785  gpg5nbgrvtx13starlem2  48786  gpg5nbgrvtx13starlem3  48787  gpg5edgnedg  48844  reorelicc  49439  rrx2plord2  49451  line2y  49484  opth2neg  49554