Theorem orel1 397

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	|- ( -. ph -> ( ( ph \/ ps ) -> ps ) )

Proof of Theorem orel1

Step	Hyp	Ref	Expression
1		pm2.53 388	. 2 |- ( ( ph \/ ps ) -> ( -. ph -> ps ) )
2	1	com12 32	1 |- ( -. ph -> ( ( ph \/ ps ) -> ps ) )

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:  pm2.25  419  biorf  420  3orel1  1041  prel12  4383  xpcan  5570  funun  5932  sorpssuni  6946  sorpssint  6947  soxp  7290  ackbij1lem18  9059  ackbij1b  9061  fincssdom  9145  fin23lem30  9164  fin1a2lem13  9234  pythagtriplem4  15524  evlslem3  19514  zringlpirlem3  19834  psgnodpm  19934  orngsqr  29804  elzdif0  30024  qqhval2lem  30025  eulerpartlemsv2  30420  eulerpartlemv  30426  eulerpartlemf  30432  eulerpartlemgh  30440  3orel13  31598  dfon2lem4  31691  dfon2lem6  31693  nosepdmlem  31833  dfrdg4  32058  rankeq1o  32278  wl-orel12  33294  poimirlem31  33440  pellfund14gap  37451  wepwsolem  37612  fmul01lt1lem1  39816  cncfiooicclem1  40106  etransclem24  40475  nnfoctbdjlem  40672