Theorem olc 855

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

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

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 199  df-or 835

This theorem is referenced by:  pm1.4  856  pm2.46  867  norbi  871  pm2.07  887  pm2.41  892  pm1.5  904  biorf  921  pm4.72  933  jaob  945  pm3.48  947  andi  991  dedlemb  1028  consensus  1034  anifp  1052  cad1  1580  19.33  1848  19.33b  1849  dfsb2  2455  dfsb2ALT  2520  mooran2  2573  undif4  4302  prel12g  4673  ordssun  6133  tpres  6796  frxp  7631  omopth2  8017  swoord1  8126  swoord2  8127  fpwwe2lem12  9867  ltapr  10271  zmulcl  11850  nn0lt2  11864  elnn1uz2  12145  mnflt  12341  mnfltpnf  12344  fzm1  12809  expeq0  13280  swrdnnn0nd  13830  nn0o1gt2  15598  prm23lt5  16013  vdwlem9  16187  cshwshashlem1  16291  cshwshash  16300  funcres2c  17041  tsrlemax  17700  odlem1  18437  gexlem1  18477  0top  21310  cmpfi  21735  alexsubALTlem3  22376  dyadmbl  23919  plydivex  24604  scvxcvx  25280  gausslemma2dlem0f  25654  nb3grprlem1  26880  1to3vfriswmgr  27829  frgrwopreg  27872  frgrregorufr  27874  frgrregord13  27968  disjunsn  30127  dfon2lem4  32591  dfrdg4  32973  broutsideof2  33144  lineunray  33169  fwddifnp1  33187  meran1  33319  bj-orim2  33448  bj-peircecurry  33450  bj-falor2  33476  bj-sbsb  33691  bj-unrab  33779  wl-orel12  34232  tsor3  34911  paddclN  36463  lcfl6  38121  sbor2  38587  ifpid3g  39295  ifpim4  39301  rp-fakeanorass  39316  iunrelexp0  39451  clsk1indlem3  39797  19.33-2  40171  ax6e2ndeq  40352  undif3VD  40675  ax6e2ndeqVD  40702  ax6e2ndeqALT  40724  stoweidlem26  41777  stoweidlem37  41788  fourierswlem  41981  fouriersw  41982  elaa2lem  41984  salexct  42083  sge0z  42123  nfunsnafv2  42865  prproropf1olem4  43071  sfprmdvdsmersenne  43171  nn0o1gt2ALTV  43262  odd2prm2  43286  even3prm2  43287  stgoldbwt  43344  nrhmzr  43543  reorelicc  44100  rrx2plord2  44112  line2y  44145