Theorem orel2 385

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 112	. 2 |- ( -. ph -> ( ph -> ps ) )
3	1, 2	jaod 382	1 |- ( -. ph -> ( ( ps \/ ph ) -> ps ) )

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

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 189  df-or 372

This theorem is referenced by:  biorfi  409  pm2.64  798  pm2.74  857  pm5.71  947  prel12  4152  xpcan2  5274  funun  5624  ablfac1eulem  17705  drngmuleq0  17998  mdetunilem9  19645  maducoeval2  19665  tdeglem4  23009  deg1sublt  23059  dgrnznn  23201  dvply1  23237  aaliou2  23296  colline  24694  axcontlem2  24995  3orel3  30344  dfrdg4  30718  arg-ax  31076  elpell14qr2  35708  elpell1qr2  35718  jm2.22  35850  jm2.23  35851  jm2.26lem3  35856  ttac  35891  wepwsolem  35900  3ornot23VD  37243  fmul01lt1lem2  37663  cncfiooicclem1  37771