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  4447  en3lplem2  7385  indpi  8499  jaoded  27385  suctrALT2VD  27662  suctrALT2  27663  en3lplem2VD  27670  hbimpgVD  27730  a9e2ndeqVD  27735  suctrALTcf  27748  suctrALTcfVD  27749  suctrALT4  27754  a9e2ndeqALT  27758
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