Theorem orc 385

Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.)

Assertion

Ref	Expression
orc

Proof of Theorem orc

Step	Hyp	Ref	Expression
1		pm2.24 109	. 2
2	1	orrd 378	1

Syntax hints:  ->wi 4  \/wo 368

This theorem is referenced by:  pm1.4  386  orcd  392  orcs  394  pm2.45  397  pm2.67-2  402  biorfi  407  pm1.5  522  pm2.4  575  pm4.44  577  pm4.45  688  pm3.48  833  orabs  855  norbi  859  andi  867  pm4.72  876  biort  896  pm5.71  936  dedlema  954  consensus  959  3mix1  1165  cad1  1465  cad11  1466  cad0  1467  19.33  1695  19.33b  1696  dfsb2  2114  moor  2347  ssun1  3666  undif3  3758  reuun1  3779  opthpr  4208  otsndisj  4757  otiunsndisj  4758  elelsuc  4955  ordelinel  4981  ordssun  4982  ordequn  4983  fununmo  5636  soxp  6913  omopth2  7252  swoord1  7359  swoord2  7360  sornom  8678  fin56  8794  fpwwe2lem12  9040  ltle  9694  nn1m1nn  10581  elnnz  10899  elnn0z  10902  zmulcl  10937  nn01to3  11204  ltpnf  11360  xrltle  11384  xrltne  11395  4sqlem17  14479  cshwsidrepswmod0  14579  cshwsdisj  14583  cshwshash  14589  funcres2c  15270  tsrlemax  15850  odlem1  16559  gexlem1  16599  drngmuleq0  17419  maducoeval2  19142  alexsubALTlem3  20549  dyadmbl  22009  bcmono  23552  nb3graprlem1  24451  frgrawopreg  25049  frgraregorufr  25053  2spotdisj  25061  2spotiundisj  25062  2spotmdisj  25068  frgraregord13  25119  dfon2lem4  29218  sltsgn1  29421  sltsgn2  29422  dfrdg4  29600  btwnconn1  29751  segcon2  29755  broutsideof2  29772  lineunray  29797  meran1  29876  dissym1  29886  wl-nftht  29989  orfa  30479  tsor2  30555  fnwe2lem3  30998  19.33-2  31287  otiunsndisjX  32301  tpres  32554  ldepspr  33074  eximp-surprise2  33200  ax6e2ndeq  33332  uunT1  33577  undif3VD  33682  ax6e2ndeqVD  33709  ax6e2ndeqALT  33731  bj-consensus  34163  bj-unrab  34494  lkrlspeqN  34896  bj-ifid1g  37708  rp-fakeanorass  37737

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 185  df-or 370