Theorem orel2 381

Description: Elimination of disjunction by denial of a disjunct. Theorem *2.56 of [WhiteheadRussell] p. 107. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Wolf Lammen, 5-Apr-2013.)

Assertion

Ref	Expression
orel2	|- ( -. ph -> ( ( ps \/ ph ) -> ps ) )

Proof of Theorem orel2

Step	Hyp	Ref	Expression
1		idd 24	. 2 |- ( -. ph -> ( ps -> ps ) )
2		pm2.21 108	. 2 |- ( -. ph -> ( ph -> ps ) )
3	1, 2	jaod 378	1 |- ( -. ph -> ( ( ps \/ ph ) -> ps ) )

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

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 368

This theorem is referenced by:  biorfi  405  pm2.64  787  pm2.74  844  pm5.71  934  prel12  4193  xpcan2  5429  funun  5612  ablfac1eulem  17318  drngmuleq0  17614  mdetunilem9  19289  maducoeval2  19309  tdeglem4  22624  deg1sublt  22677  dgrnznn  22810  dvply1  22846  aaliou2  22902  colline  24231  axcontlem2  24470  3orel3  29330  dfrdg4  29828  arg-ax  30109  elpell14qr2  31037  elpell1qr2  31047  jm2.22  31176  jm2.23  31177  jm2.26lem3  31182  ttac  31217  wepwsolem  31226  fmul01lt1lem2  31818  cncfiooicclem1  31935  3ornot23VD  34047