Theorem olc 864

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

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

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 206  df-or 844

This theorem is referenced by:  pm1.4  865  pm2.46  879  norbi  883  pm2.07  899  pm2.41  904  pm1.5  916  biorf  933  pm4.72  946  jaob  958  pm3.48  960  andi  1004  dedlemb  1043  consensus  1049  anifp  1068  norassOLD  1536  cad1  1620  19.33  1888  19.33b  1889  dfsb2  2497  mooran2  2556  undif4  4397  prel12g  4791  ordssun  6350  tpres  7058  frxp  7938  omopth2  8377  swoord1  8487  swoord2  8488  fpwwe2lem11  10328  ltapr  10732  zmulcl  12299  nn0lt2  12313  elnn1uz2  12594  mnflt  12788  mnfltpnf  12791  fzm1  13265  expeq0  13741  swrdnnn0nd  14297  nn0o1gt2  16018  prm23lt5  16443  vdwlem9  16618  cshwshashlem1  16725  cshwshash  16734  funcres2c  17533  tsrlemax  18219  odlem1  19058  gexlem1  19099  0top  22041  cmpfi  22467  alexsubALTlem3  23108  dyadmbl  24669  plydivex  25362  scvxcvx  26040  gausslemma2dlem0f  26414  nb3grprlem1  27650  1to3vfriswmgr  28545  frgrwopreg  28588  frgrregorufr  28590  frgrregord13  28661  disjunsn  30834  dfon2lem4  33668  frxp2  33718  frxp3  33724  dfrdg4  34180  broutsideof2  34351  lineunray  34376  fwddifnp1  34394  meran1  34527  bj-orim2  34663  bj-peircecurry  34665  bj-falor2  34694  bj-sbsb  34947  bj-unrab  35041  wl-orel12  35597  tsor3  36234  paddclN  37783  lcfl6  39441  sbor2  40105  fsuppind  40202  ifpid3g  40997  ifpim4  41003  rp-fakeanorass  41018  sqrtcval  41138  iunrelexp0  41199  clsk1indlem3  41542  19.33-2  41889  ax6e2ndeq  42068  undif3VD  42391  ax6e2ndeqVD  42418  ax6e2ndeqALT  42440  stoweidlem26  43457  stoweidlem37  43468  fourierswlem  43661  fouriersw  43662  elaa2lem  43664  salexct  43763  sge0z  43803  nfunsnafv2  44604  prproropf1olem4  44846  sfprmdvdsmersenne  44943  nn0o1gt2ALTV  45034  odd2prm2  45058  even3prm2  45059  stgoldbwt  45116  nrhmzr  45319  reorelicc  45944  rrx2plord2  45956  line2y  45989