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

Theorem olc 399
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 393 1 (𝜑 → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 383
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 197  df-or 385
This theorem is referenced by:  pm1.4  401  pm2.07  411  pm2.46  413  biorf  420  pm1.5  544  pm2.41  596  jaob  821  pm3.48  877  norbi  903  andi  910  pm4.72  919  consensus  998  dedlemb  1002  anifp  1019  cad1  1553  nfntht  1717  nfntht2  1718  19.33  1810  19.33b  1811  dfsb2  2371  mooran2  2526  undif3OLD  3881  undif4  4026  ordelinelOLD  5814  ordssun  5815  tpres  6451  frxp  7272  omopth2  7649  swoord1  7758  swoord2  7759  rankxplim3  8729  fpwwe2lem12  9448  ltapr  9852  zmulcl  11411  nn0lt2  11425  elnn1uz2  11750  mnflt  11942  mnfltpnf  11945  fzm1  12404  expeq0  12873  nn0o1gt2  15078  prm23lt5  15500  vdwlem9  15674  cshwshashlem1  15783  cshwshash  15792  funcres2c  16542  tsrlemax  17201  odlem1  17935  gexlem1  17975  0top  20768  cmpfi  21192  alexsubALTlem3  21834  dyadmbl  23349  plydivex  24033  scvxcvx  24693  gausslemma2dlem0f  25067  nb3grprlem1  26263  1to3vfriswmgr  27124  frgrwopreg  27159  frgrregorufr  27163  frgrregord13  27224  disjunsn  29379  dfon2lem4  31665  dfrdg4  32033  broutsideof2  32204  lineunray  32229  fwddifnp1  32247  meran1  32385  bj-orim2  32516  bj-currypeirce  32519  bj-peircecurry  32520  bj-falor2  32545  bj-sbsb  32799  bj-unrab  32897  wl-orel12  33265  tsor3  33927  paddclN  34947  lcfl6  36608  ifpid3g  37656  ifpim4  37662  rp-fakeanorass  37677  iunrelexp0  37813  clsk1indlem3  38161  19.33-2  38401  ax6e2ndeq  38595  undif3VD  38938  ax6e2ndeqVD  38965  ax6e2ndeqALT  38987  disjxp1  39058  stoweidlem26  40006  stoweidlem37  40017  fourierswlem  40210  fouriersw  40211  elaa2lem  40213  salexct  40315  sge0z  40355  sfprmdvdsmersenne  41285  nn0o1gt2ALTV  41370  odd2prm2  41392  even3prm2  41393  stgoldbwt  41429  nrhmzr  41638
  Copyright terms: Public domain W3C validator