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

Theorem olc 397
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 391 1 (𝜑 → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 381
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 195  df-or 383
This theorem is referenced by:  pm1.4  399  pm2.07  409  pm2.46  411  biorf  418  pm1.5  542  pm2.41  594  jaob  817  pm3.48  873  norbi  899  andi  906  pm4.72  915  consensus  989  dedlemb  993  anifp  1013  cad1  1545  nfntht  1708  nfntht2  1709  19.33  1799  19.33b  1800  dfsb2  2356  mooran2  2511  undif3OLD  3843  undif4  3982  ordelinelOLD  5725  ordssun  5726  tpres  6345  frxp  7147  omopth2  7524  swoord1  7633  swoord2  7634  rankxplim3  8600  fpwwe2lem12  9315  ltapr  9719  zmulcl  11255  nn0lt2  11269  elnn1uz2  11593  mnflt  11790  mnfltpnf  11793  fzm1  12240  expeq0  12703  nn0o1gt2  14877  prm23lt5  15299  vdwlem9  15473  cshwshashlem1  15582  cshwshash  15591  funcres2c  16326  tsrlemax  16985  odlem1  17719  gexlem1  17759  0top  20536  cmpfi  20959  alexsubALTlem3  21601  dyadmbl  23087  plydivex  23769  scvxcvx  24425  gausslemma2dlem0f  24799  nb3graprlem1  25742  uvtx01vtx  25782  1to3vfriswmgra  26296  frgraregorufr  26342  frgraregord13  26408  disjunsn  28591  dfon2lem4  30737  sltsgn1  30860  sltsgn2  30861  dfrdg4  31030  broutsideof2  31201  lineunray  31226  fwddifnp1  31244  meran1  31382  bj-orim2  31513  bj-currypeirce  31516  bj-peircecurry  31517  bj-falor2  31545  bj-nfntht  31572  bj-nfntht2  31573  bj-sbsb  31821  bj-unrab  31913  wl-orel12  32272  tsor3  32925  paddclN  33945  lcfl6  35606  ifpid3g  36655  ifpim4  36661  rp-fakeanorass  36676  iunrelexp0  36812  clsk1indlem3  37160  19.33-2  37402  ax6e2ndeq  37595  undif3VD  37939  ax6e2ndeqVD  37966  ax6e2ndeqALT  37988  disjxp1  38062  nelpr2  38087  stoweidlem26  38719  stoweidlem37  38730  fourierswlem  38923  fouriersw  38924  elaa2lem  38926  salexct  39028  sge0z  39068  sfprmdvdsmersenne  39859  nn0o1gt2ALTV  39944  stgoldbwt  39999  nb3grprlem1  40606  1to3vfriswmgr  41448  frgrregorufr  41488  av-frgraregord13  41548  nrhmzr  41661
  Copyright terms: Public domain W3C validator