Theorem olc 881

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 860

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 861

This theorem is used by:  pm1.4  882  pm2.46  895  norbi  899  pm2.07  915  pm2.41  920  pm1.5  932  biorf  949  pm4.72  963  jaob  975  pm3.48  977  andi  1024  dedlemb  1061  consensus  1067  anifp  1087  cad1  1646  19.33  1913  19.33b  1914  dfsb2  2524  mooran2  2583  undif4  4426  prel12g  4828  ordssun  6465  tpres  7199  fvf1pr  7305  frxp  8120  frxp2  8138  frxp3  8145  omopth2  8567  naddunif  8678  swoord1  8725  swoord2  8726  fpwwe2lem11  10632  ltapr  11036  zmulcl  12649  nn0lt2  12665  elnn1uz2  12955  mnflt  13154  mnfltpnf  13157  fzm1  13642  expeq0  14135  zzlesq  14249  swrdnnn0nd  14701  nn0o1gt2  16445  prm23lt5  16880  vdwlem9  17055  cshwshashlem1  17161  cshwshash  17170  funcres2c  17966  tsrlemax  18648  odlem1  19611  gexlem1  19655  nrhmzr  20647  0top  23151  cmpfi  23576  alexsubALTlem3  24217  dyadmbl  25770  plydivex  26469  scvxcvx  27161  gausslemma2dlem0f  27536  nb3grprlem1  29741  1to3vfriswmgr  30642  frgrwopreg  30685  frgrregorufr  30687  frgrregord13  30758  disjunsn  32950  axprALT2  35512  dfon2lem4  36284  dfrdg4  36451  broutsideof2  36622  lineunray  36647  fwddifnp1  36665  meran1  36950  axtco1from2  37014  bj-orim2  37176  bj-peircecurry  37178  bj-falor2  37206  bj-sbsb  37500  bj-unrab  37590  wl-orel12  38194  tsor3  38826  paddclN  40644  lcfl6  42302  quadfac  43000  sbor2  43009  fsuppind  43350  omcl3g  44089  ifpid3g  44246  ifpim4  44252  rp-fakeanorass  44267  sqrtcval  44395  iunrelexp0  44456  clsk1indlem3  44797  19.33-2  45120  ax6e2ndeq  45296  undif3VD  45618  ax6e2ndeqVD  45645  ax6e2ndeqALT  45667  stoweidlem26  46768  stoweidlem37  46779  fourierswlem  46972  fouriersw  46973  elaa2lem  46975  salexct  47076  sge0z  47117  nfunsnafv2  47990  prproropf1olem4  48283  sfprmdvdsmersenne  48383  nn0o1gt2ALTV  48487  odd2prm2  48511  even3prm2  48512  stgoldbwt  48569  clnbgrel  48621  gpg5nbgrvtx03starlem1  48861  gpg5nbgrvtx03starlem2  48862  gpg5nbgrvtx03starlem3  48863  gpg5nbgrvtx13starlem1  48864  gpg5nbgrvtx13starlem2  48865  gpg5nbgrvtx13starlem3  48866  gpg5edgnedg  48923  reorelicc  49518  rrx2plord2  49530  line2y  49563  opth2neg  49633