Theorem olc 882

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

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

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 862

This theorem is used by:  pm1.4  883  pm2.46  896  norbi  900  pm2.07  916  pm2.41  921  pm1.5  933  biorf  950  pm4.72  964  jaob  976  pm3.48  978  andi  1025  dedlemb  1062  consensus  1068  anifp  1088  cad1  1650  19.33  1917  19.33b  1918  dfsb2  2522  mooran2  2581  undif4  4419  prel12g  4823  ordssun  6456  tpres  7195  fvf1pr  7303  frxp  8121  frxp2  8139  frxp3  8146  omopth2  8570  naddunif  8681  swoord1  8728  swoord2  8729  fpwwe2lem11  10697  ltapr  11101  zmulcl  12714  nn0lt2  12731  elnn1uz2  13021  mnflt  13221  mnfltpnf  13224  fzm1  13709  expeq0  14203  zzlesq  14317  swrdnnn0nd  14773  nn0o1gt2  16518  prm23lt5  16953  vdwlem9  17128  cshwshashlem1  17234  cshwshash  17243  funcres2c  18039  tsrlemax  18721  odlem1  19710  gexlem1  19754  nrhmzr  20750  0top  23262  cmpfi  23687  alexsubALTlem3  24329  dyadmbl  25882  plydivex  26581  scvxcvx  27276  gausslemma2dlem0f  27651  nb3grprlem1  29894  1to3vfriswmgr  30814  frgrwopreg  30857  frgrregorufr  30859  frgrregord13  30930  disjunsn  33121  axprALT2  35664  dfon2lem4  36470  dfrdg4  36637  broutsideof2  36809  lineunray  36834  fwddifnp1  36852  meran1  37121  axtco1from2  37185  bj-orim2  37347  bj-peircecurry  37349  bj-falor2  37377  bj-sbsb  37671  bj-unrab  37761  wl-orel12  38363  impprop  38564  tsor3  39001  paddclN  40819  lcfl6  42477  quadfac  43175  sbor2  43184  fsuppind  43540  omcl3g  44279  ifpid3g  44436  ifpim4  44442  rp-fakeanorass  44457  sqrtcval  44585  iunrelexp0  44646  clsk1indlem3  44987  19.33-2  45310  ax6e2ndeq  45486  undif3VD  45808  ax6e2ndeqVD  45835  ax6e2ndeqALT  45857  stoweidlem26  46958  stoweidlem37  46969  fourierswlem  47162  fouriersw  47163  elaa2lem  47165  salexct  47266  sge0z  47307  nfunsnafv2  48217  prproropf1olem4  48510  sfprmdvdsmersenne  48610  nn0o1gt2ALTV  48714  odd2prm2  48738  even3prm2  48739  stgoldbwt  48796  clnbgrel  48848  gpg5nbgrvtx03starlem1  49088  gpg5nbgrvtx03starlem2  49089  gpg5nbgrvtx03starlem3  49090  gpg5nbgrvtx13starlem1  49091  gpg5nbgrvtx13starlem2  49092  gpg5nbgrvtx13starlem3  49093  gpg5edgnedg  49150  reorelicc  49744  rrx2plord2  49756  line2y  49789  opth2neg  49859