Theorem orel2 383

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

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

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

This theorem is referenced by:  biorfi  407  pm2.64  787  pm2.74  842  pm5.71  927  prel12  4044  xpcan2  5270  funun  5455  ablfac1eulem  16561  drngmuleq0  16833  mdetunilem9  18401  maducoeval2  18421  tdeglem4  21504  deg1sublt  21557  dvply1  21725  aaliou2  21781  colline  23020  axcontlem2  23162  3orel3  27319  dfrdg4  27932  arg-ax  28214  elpell14qr2  29156  elpell1qr2  29166  jm2.22  29297  jm2.23  29298  jm2.26lem3  29303  ttac  29338  wepwsolem  29347  dgrnznn  29445  fmul01lt1lem2  29719  3ornot23VD  31470