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

Theorem jao 498
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 497 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ch  ->  ps ) )  ->  (
( ph  \/  ch )  ->  ps ) )
21ex 423 1  |-  ( (
ph  ->  ps )  -> 
( ( ch  ->  ps )  ->  ( ( ph  \/  ch )  ->  ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357
This theorem is referenced by:  3jao  1243  suctr  4475  en3lplem2  7417  indpi  8531  jaoded  28332  suctrALT2VD  28612  suctrALT2  28613  en3lplem2VD  28620  hbimpgVD  28680  a9e2ndeqVD  28685  suctrALTcf  28698  suctrALTcfVD  28699  suctrALT4  28704  a9e2ndeqALT  28708
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360
  Copyright terms: Public domain W3C validator