Theorem orel1 382

Description: Elimination of disjunction by denial of a disjunct. Theorem *2.55 of [WhiteheadRussell] p. 107. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Wolf Lammen, 21-Jul-2012.)

Assertion

Ref	Expression
orel1

Proof of Theorem orel1

Step	Hyp	Ref	Expression
1		pm2.53 373	. 2
2	1	com12 31	1

Syntax hints:  -.wn 3  ->wi 4  \/wo 368

This theorem is referenced by:  pm2.25  404  biorf  405  ornldOLD  899  prel12  4207  xpcan  5448  funun  5635  sorpssuni  6589  sorpssint  6590  soxp  6913  ackbij1lem18  8638  ackbij1b  8640  fincssdom  8724  fin23lem30  8743  fin1a2lem13  8813  pythagtriplem4  14343  evlslem3  18183  zringlpirlem3  18511  zlpirlem3  18516  psgnodpm  18624  orngsqr  27794  elzdif0  27961  qqhval2lem  27962  eulerpartlemsv2  28297  eulerpartlemv  28303  eulerpartlemf  28309  eulerpartlemgh  28317  3orel1  29087  3orel13  29094  dfon2lem4  29218  dfon2lem6  29220  dfrdg4  29600  rankeq1o  29828  pellfund14gap  30823  wepwsolem  30987  fmul01lt1lem1  31578  cncfiooicclem1  31696  etransclem24  32041

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