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  2497  mooran2  2556  undif4  4407  prel12g  4807  ordssun  6427  tpres  7156  fvf1pr  7262  frxp  8076  frxp2  8094  frxp3  8101  omopth2  8519  naddunif  8629  swoord1  8676  swoord2  8677  fpwwe2lem11  10564  ltapr  10968  zmulcl  12576  nn0lt2  12592  elnn1uz2  12875  mnflt  13074  mnfltpnf  13077  fzm1  13561  expeq0  14054  zzlesq  14168  swrdnnn0nd  14619  nn0o1gt2  16350  prm23lt5  16785  vdwlem9  16960  cshwshashlem1  17066  cshwshash  17075  funcres2c  17870  tsrlemax  18552  odlem1  19510  gexlem1  19554  nrhmzr  20514  0top  22948  cmpfi  23373  alexsubALTlem3  24014  dyadmbl  25567  plydivex  26263  scvxcvx  26949  gausslemma2dlem0f  27324  nb3grprlem1  29449  1to3vfriswmgr  30350  frgrwopreg  30393  frgrregorufr  30395  frgrregord13  30466  disjunsn  32664  axprALT2  35253  dfon2lem4  35966  dfrdg4  36133  broutsideof2  36304  lineunray  36329  fwddifnp1  36347  meran1  36593  axtco1from2  36657  bj-orim2  36820  bj-peircecurry  36822  bj-falor2  36850  bj-sbsb  37144  bj-unrab  37233  wl-orel12  37836  tsor3  38470  paddclN  40288  lcfl6  41946  sbor2  42651  fsuppind  43023  omcl3g  43762  ifpid3g  43919  ifpim4  43925  rp-fakeanorass  43940  sqrtcval  44068  iunrelexp0  44129  clsk1indlem3  44470  19.33-2  44809  ax6e2ndeq  44986  undif3VD  45308  ax6e2ndeqVD  45335  ax6e2ndeqALT  45357  stoweidlem26  46454  stoweidlem37  46465  fourierswlem  46658  fouriersw  46659  elaa2lem  46661  salexct  46762  sge0z  46803  nfunsnafv2  47673  prproropf1olem4  47966  sfprmdvdsmersenne  48066  nn0o1gt2ALTV  48170  odd2prm2  48194  even3prm2  48195  stgoldbwt  48252  clnbgrel  48304  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpg5edgnedg  48606  reorelicc  49186  rrx2plord2  49198  line2y  49231  opth2neg  49302