Theorem orel2 384

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 25	. 2 |- ( -. ph -> ( ps -> ps ) )
2		pm2.21 111	. 2 |- ( -. ph -> ( ph -> ps ) )
3	1, 2	jaod 381	1 |- ( -. ph -> ( ( ps \/ ph ) -> ps ) )

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

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 188  df-or 371

This theorem is referenced by:  biorfi  408  pm2.64  796  pm2.74  854  pm5.71  944  prel12  4171  xpcan2  5285  funun  5634  ablfac1eulem  17633  drngmuleq0  17926  mdetunilem9  19569  maducoeval2  19589  tdeglem4  22883  deg1sublt  22933  dgrnznn  23066  dvply1  23102  aaliou2  23158  colline  24551  axcontlem2  24838  3orel3  30129  dfrdg4  30500  arg-ax  30858  elpell14qr2  35418  elpell1qr2  35428  jm2.22  35560  jm2.23  35561  jm2.26lem3  35566  ttac  35601  wepwsolem  35610  3ornot23VD  36887  fmul01lt1lem2  37239  cncfiooicclem1  37347