Theorem olc 398

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

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

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 197  df-or 384

This theorem is referenced by:  pm1.4  400  pm2.07  410  pm2.46  412  biorf  419  pm1.5  545  pm2.41  598  jaob  857  pm3.48  914  norbi  940  andi  947  pm4.72  956  annotanannotOLD  978  dedlemb  1033  consensus  1041  anifp  1058  cad1  1692  nfntht  1856  nfntht2  1857  19.33  1949  19.33b  1950  dfsb2  2498  mooran2  2654  undif3OLD  4020  undif4  4167  prel12g  4532  ordelinelOLD  5975  ordssun  5976  tpres  6618  frxp  7443  omopth2  7821  swoord1  7930  swoord2  7931  rankxplim3  8905  fpwwe2lem12  9626  ltapr  10030  zmulcl  11589  nn0lt2  11603  elnn1uz2  11929  mnflt  12121  mnfltpnf  12124  fzm1  12584  expeq0  13055  nn0o1gt2  15270  prm23lt5  15692  vdwlem9  15866  cshwshashlem1  15975  cshwshash  15984  funcres2c  16733  tsrlemax  17392  odlem1  18125  gexlem1  18165  0top  20960  cmpfi  21384  alexsubALTlem3  22025  dyadmbl  23539  plydivex  24222  scvxcvx  24882  gausslemma2dlem0f  25256  nb3grprlem1  26451  1to3vfriswmgr  27405  frgrwopreg  27448  frgrregorufr  27450  frgrregord13  27535  disjunsn  29685  dfon2lem4  31967  dfrdg4  32335  broutsideof2  32506  lineunray  32531  fwddifnp1  32549  meran1  32687  bj-orim2  32818  bj-currypeirce  32821  bj-peircecurry  32822  bj-falor2  32847  bj-sbsb  33101  bj-unrab  33199  wl-orel12  33576  tsor3  34238  paddclN  35600  lcfl6  37260  ifpid3g  38308  ifpim4  38314  rp-fakeanorass  38329  iunrelexp0  38465  clsk1indlem3  38812  19.33-2  39052  ax6e2ndeq  39246  undif3VD  39586  ax6e2ndeqVD  39613  ax6e2ndeqALT  39635  disjxp1  39706  stoweidlem26  40715  stoweidlem37  40726  fourierswlem  40919  fouriersw  40920  elaa2lem  40922  salexct  41024  sge0z  41064  sfprmdvdsmersenne  41999  nn0o1gt2ALTV  42084  odd2prm2  42106  even3prm2  42107  stgoldbwt  42143  nrhmzr  42352