MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jao Unicode version

Theorem jao 500
Description: Disjunction of antecedents. Compare Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 4-Apr-2013.)
Assertion
Ref Expression
jao  |-  ( (
ph  ->  ps )  -> 
( ( ch  ->  ps )  ->  ( ( ph  \/  ch )  ->  ps ) ) )

Proof of Theorem jao
StepHypRef Expression
1 pm3.44 499 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ch  ->  ps ) )  ->  (
( ph  \/  ch )  ->  ps ) )
21ex 425 1  |-  ( (
ph  ->  ps )  -> 
( ( ch  ->  ps )  ->  ( ( ph  \/  ch )  ->  ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    \/ wo 359
This theorem is referenced by:  3jao  1248  suctr  4368  en3lplem2  7301  indpi  8411  jaoded  27025  suctrALT2VD  27302  suctrALT2  27303  en3lplem2VD  27310  hbimpgVD  27370  a9e2ndeqVD  27375  suctrALTcf  27388  suctrALTcfVD  27389  suctrALT4  27394  a9e2ndeqALT  27398
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362
  Copyright terms: Public domain W3C validator