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

Theorem jao 499
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 498 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ch  ->  ps ) )  ->  (
( ph  \/  ch )  ->  ps ) )
21ex 424 1  |-  ( (
ph  ->  ps )  -> 
( ( ch  ->  ps )  ->  ( ( ph  \/  ch )  ->  ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358
This theorem is referenced by:  3jao  1245  suctr  4656  en3lplem2  7660  indpi  8773  jaoded  28508  suctrALT2VD  28802  suctrALT2  28803  en3lplem2VD  28810  hbimpgVD  28870  a9e2ndeqVD  28875  suctrALTcf  28888  suctrALTcfVD  28889  a9e2ndeqALT  28898
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 178  df-or 360  df-an 361
  Copyright terms: Public domain W3C validator