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  4421  prel12g  4822  ordssun  6431  tpres  7159  fvf1pr  7265  frxp  8080  frxp2  8098  frxp3  8105  omopth2  8523  naddunif  8633  swoord1  8680  swoord2  8681  fpwwe2lem11  10566  ltapr  10970  zmulcl  12554  nn0lt2  12569  elnn1uz2  12852  mnflt  13051  mnfltpnf  13054  fzm1  13537  expeq0  14029  zzlesq  14143  swrdnnn0nd  14594  nn0o1gt2  16322  prm23lt5  16756  vdwlem9  16931  cshwshashlem1  17037  cshwshash  17046  funcres2c  17841  tsrlemax  18523  odlem1  19481  gexlem1  19525  nrhmzr  20487  0top  22944  cmpfi  23369  alexsubALTlem3  24010  dyadmbl  25574  plydivex  26278  scvxcvx  26969  gausslemma2dlem0f  27345  nb3grprlem1  29471  1to3vfriswmgr  30373  frgrwopreg  30416  frgrregorufr  30418  frgrregord13  30489  disjunsn  32687  axprALT2  35293  dfon2lem4  36006  dfrdg4  36173  broutsideof2  36344  lineunray  36369  fwddifnp1  36387  meran1  36633  bj-orim2  36788  bj-peircecurry  36790  bj-falor2  36818  bj-sbsb  37112  bj-unrab  37201  wl-orel12  37795  tsor3  38429  paddclN  40247  lcfl6  41905  sbor2  42611  fsuppind  42977  omcl3g  43720  ifpid3g  43877  ifpim4  43883  rp-fakeanorass  43898  sqrtcval  44026  iunrelexp0  44087  clsk1indlem3  44428  19.33-2  44767  ax6e2ndeq  44944  undif3VD  45266  ax6e2ndeqVD  45293  ax6e2ndeqALT  45315  stoweidlem26  46413  stoweidlem37  46424  fourierswlem  46617  fouriersw  46618  elaa2lem  46620  salexct  46721  sge0z  46762  nfunsnafv2  47614  prproropf1olem4  47895  sfprmdvdsmersenne  47992  nn0o1gt2ALTV  48083  odd2prm2  48107  even3prm2  48108  stgoldbwt  48165  clnbgrel  48217  gpg5nbgrvtx03starlem1  48457  gpg5nbgrvtx03starlem2  48458  gpg5nbgrvtx03starlem3  48459  gpg5nbgrvtx13starlem1  48460  gpg5nbgrvtx13starlem2  48461  gpg5nbgrvtx13starlem3  48462  gpg5edgnedg  48519  reorelicc  49099  rrx2plord2  49111  line2y  49144  opth2neg  49215