Theorem olc 869

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

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

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 849

This theorem is referenced by:  pm1.4  870  pm2.46  883  norbi  887  pm2.07  903  pm2.41  908  pm1.5  920  biorf  937  pm4.72  952  jaob  964  pm3.48  966  andi  1010  dedlemb  1047  consensus  1053  anifp  1072  cad1  1619  19.33  1886  19.33b  1887  dfsb2  2498  mooran2  2557  undif4  4420  prel12g  4821  ordssun  6422  tpres  7149  fvf1pr  7255  frxp  8070  frxp2  8088  frxp3  8095  omopth2  8513  naddunif  8623  swoord1  8670  swoord2  8671  fpwwe2lem11  10556  ltapr  10960  zmulcl  12544  nn0lt2  12559  elnn1uz2  12842  mnflt  13041  mnfltpnf  13044  fzm1  13527  expeq0  14019  zzlesq  14133  swrdnnn0nd  14584  nn0o1gt2  16312  prm23lt5  16746  vdwlem9  16921  cshwshashlem1  17027  cshwshash  17036  funcres2c  17831  tsrlemax  18513  odlem1  19468  gexlem1  19512  nrhmzr  20474  0top  22931  cmpfi  23356  alexsubALTlem3  23997  dyadmbl  25561  plydivex  26265  scvxcvx  26956  gausslemma2dlem0f  27332  nb3grprlem1  29457  1to3vfriswmgr  30359  frgrwopreg  30402  frgrregorufr  30404  frgrregord13  30475  disjunsn  32672  dfon2lem4  35980  dfrdg4  36147  broutsideof2  36318  lineunray  36343  fwddifnp1  36361  meran1  36607  bj-orim2  36758  bj-peircecurry  36760  bj-falor2  36787  bj-sbsb  37040  bj-unrab  37129  wl-orel12  37718  tsor3  38352  paddclN  40170  lcfl6  41828  sbor2  42534  fsuppind  42900  omcl3g  43643  ifpid3g  43800  ifpim4  43806  rp-fakeanorass  43821  sqrtcval  43949  iunrelexp0  44010  clsk1indlem3  44351  19.33-2  44690  ax6e2ndeq  44867  undif3VD  45189  ax6e2ndeqVD  45216  ax6e2ndeqALT  45238  stoweidlem26  46337  stoweidlem37  46348  fourierswlem  46541  fouriersw  46542  elaa2lem  46544  salexct  46645  sge0z  46686  nfunsnafv2  47538  prproropf1olem4  47819  sfprmdvdsmersenne  47916  nn0o1gt2ALTV  48007  odd2prm2  48031  even3prm2  48032  stgoldbwt  48089  clnbgrel  48141  gpg5nbgrvtx03starlem1  48381  gpg5nbgrvtx03starlem2  48382  gpg5nbgrvtx03starlem3  48383  gpg5nbgrvtx13starlem1  48384  gpg5nbgrvtx13starlem2  48385  gpg5nbgrvtx13starlem3  48386  gpg5edgnedg  48443  reorelicc  49023  rrx2plord2  49035  line2y  49068  opth2neg  49139