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

Theorem orc 387
Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
orc  |-  ( ph  ->  ( ph  \/  ps ) )

Proof of Theorem orc
StepHypRef Expression
1 pm2.24 113 . 2  |-  ( ph  ->  ( -.  ph  ->  ps ) )
21orrd 380 1  |-  ( ph  ->  ( ph  \/  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 370
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 189  df-or 372
This theorem is referenced by:  pm1.4  388  orcd  394  orcs  396  pm2.45  399  pm2.67-2  404  biorfi  409  pm1.5  525  pm2.4  579  pm4.44  581  pm4.45  694  pm3.48  844  orabs  866  norbi  870  andi  878  pm4.72  887  biort  907  pm5.71  947  dedlema  965  consensus  970  3mix1  1177  ifptru  1436  cad0  1520  cad11  1522  19.33  1747  19.33b  1748  dfsb2  2202  moor  2355  ssun1  3597  undif3  3704  reuun1  3725  eqoreldif  4013  opthpr  4153  otsndisj  4706  otiunsndisj  4707  elelsuc  5495  ordelinel  5521  ordssun  5522  ordequn  5523  fununmo  5625  tpres  6117  soxp  6909  omopth2  7285  swoord1  7392  swoord2  7393  sornom  8707  fin56  8823  fpwwe2lem12  9066  ltle  9722  nn1m1nn  10629  elnnz  10947  elnn0z  10950  zmulcl  10985  nn01to3  11257  ltpnf  11422  xrltle  11448  xrltne  11460  4sqlem17OLD  14905  4sqlem17  14911  cshwsidrepswmod0  15065  cshwsdisj  15069  cshwshash  15075  funcres2c  15806  tsrlemax  16466  odlem1  17181  odlem1OLD  17184  gexlem1  17228  gexlem1OLD  17230  drngmuleq0  17998  maducoeval2  19665  alexsubALTlem3  21064  dyadmbl  22558  bcmono  24205  nb3graprlem1  25179  frgrawopreg  25777  frgraregorufr  25781  2spotdisj  25789  2spotiundisj  25790  2spotmdisj  25796  frgraregord13  25847  dfon2lem4  30432  sltsgn1  30548  sltsgn2  30549  dfrdg4  30718  btwnconn1  30868  segcon2  30872  broutsideof2  30889  lineunray  30914  meran1  31071  dissym1  31081  bj-consensus  31156  bj-unrab  31529  wl-orel12  31849  wl-nftht  31869  orfa  32315  tsor2  32390  lkrlspeqN  32737  fnwe2lem3  35910  ifpid1g  36138  ifpim3  36140  rp-fakeanorass  36157  19.33-2  36731  ax6e2ndeq  36926  uunT1  37167  undif3VD  37279  ax6e2ndeqVD  37306  ax6e2ndeqALT  37328  disjxp1  37411  salexct  38193  salexct3  38201  salgencntex  38202  salgensscntex  38203  nnfoctbdjlem  38293  nn0o1gt2ALTV  38823  otiunsndisjX  39006  nb3grprlem1  39454  ldepspr  40319  elfzolborelfzop1  40369  nn0o1gt2  40380  blen1b  40452  eximp-surprise2  40577
  Copyright terms: Public domain W3C validator