MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  olc Structured version   Visualization version   GIF version

Theorem olc 894
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
StepHypRef Expression
1 ax-1 6 . 2 (𝜑 → (¬ 𝜓𝜑))
21orrd 889 1 (𝜑 → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 873
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 198  df-or 874
This theorem is referenced by:  pm1.4  895  pm2.46  906  norbi  910  pm2.07  926  pm2.41  931  pm1.5  943  biorf  960  pm4.72  972  jaob  984  pm3.48  986  andi  1030  annotanannotOLD  1034  dedlemb  1069  consensus  1075  anifp  1093  cad1  1725  19.33  1983  19.33b  1984  dfsb2  2461  mooran2  2649  undif4  4194  prel12g  4549  ordssun  6006  tpres  6658  frxp  7488  omopth2  7868  swoord1  7977  swoord2  7978  rankxplim3  8958  fpwwe2lem12  9715  ltapr  10119  zmulcl  11672  nn0lt2  11686  elnn1uz2  11965  mnflt  12156  mnfltpnf  12159  fzm1  12626  expeq0  13096  nn0o1gt2  15380  prm23lt5  15799  vdwlem9  15973  cshwshashlem1  16077  cshwshash  16086  funcres2c  16827  tsrlemax  17487  odlem1  18219  gexlem1  18259  0top  21066  cmpfi  21490  alexsubALTlem3  22131  dyadmbl  23657  plydivex  24342  scvxcvx  25002  gausslemma2dlem0f  25376  nb3grprlem1  26560  1to3vfriswmgr  27517  frgrwopreg  27560  frgrregorufr  27562  frgrregord13  27646  disjunsn  29789  dfon2lem4  32065  dfrdg4  32433  broutsideof2  32604  lineunray  32629  fwddifnp1  32647  meran1  32780  bj-orim2  32910  bj-currypeirce  32912  bj-peircecurry  32913  bj-falor2  32937  bj-sbsb  33185  bj-unrab  33282  wl-orel12  33659  tsor3  34309  paddclN  35730  lcfl6  37388  ifpid3g  38445  ifpim4  38451  rp-fakeanorass  38466  iunrelexp0  38601  clsk1indlem3  38947  19.33-2  39187  ax6e2ndeq  39369  undif3VD  39702  ax6e2ndeqVD  39729  ax6e2ndeqALT  39751  disjxp1  39821  stoweidlem26  40812  stoweidlem37  40823  fourierswlem  41016  fouriersw  41017  elaa2lem  41019  salexct  41121  sge0z  41161  nfunsnafv2  41905  sfprmdvdsmersenne  42128  nn0o1gt2ALTV  42213  odd2prm2  42235  even3prm2  42236  stgoldbwt  42272  nrhmzr  42474
  Copyright terms: Public domain W3C validator