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  27122  suctrALT2VD  27399  suctrALT2  27400  en3lplem2VD  27407  hbimpgVD  27467  a9e2ndeqVD  27472  suctrALTcf  27485  suctrALTcfVD  27486  suctrALT4  27491  a9e2ndeqALT  27495
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