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

Theorem 3jaoi 1247
Description: Disjunction of 3 antecedents (inference). (Contributed by NM, 12-Sep-1995.)
Hypotheses
Ref Expression
3jaoi.1  |-  ( ph  ->  ps )
3jaoi.2  |-  ( ch 
->  ps )
3jaoi.3  |-  ( th 
->  ps )
Assertion
Ref Expression
3jaoi  |-  ( (
ph  \/  ch  \/  th )  ->  ps )

Proof of Theorem 3jaoi
StepHypRef Expression
1 3jaoi.1 . . 3  |-  ( ph  ->  ps )
2 3jaoi.2 . . 3  |-  ( ch 
->  ps )
3 3jaoi.3 . . 3  |-  ( th 
->  ps )
41, 2, 33pm3.2i 1132 . 2  |-  ( (
ph  ->  ps )  /\  ( ch  ->  ps )  /\  ( th  ->  ps ) )
5 3jao 1245 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ch  ->  ps )  /\  ( th 
->  ps ) )  -> 
( ( ph  \/  ch  \/  th )  ->  ps ) )
64, 5ax-mp 8 1  |-  ( (
ph  \/  ch  \/  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ w3o 935    /\ w3a 936
This theorem is referenced by:  3jaoian  1249  ordzsl  4792  onzsl  4793  tfrlem16  6621  oawordeulem  6764  elfiun  7401  domtriomlem  8286  axdc3lem2  8295  rankcf  8616  znegcl  10277  xrltnr  10684  xnegcl  10763  xnegneg  10764  xltnegi  10766  xnegid  10786  xaddid1  10789  xmulid1  10822  xrsupsslem  10849  xrinfmsslem  10850  elfznelfzo  11155  hashtpg  11654  ioombl1  19417  ppiublem1  20947  ostth  21294  nb3graprlem1  21421  kur14lem7  24859  3jaodd  25129  dfrdg2  25374  sltval2  25532  sltsgn1  25537  sltsgn2  25538  sltintdifex  25539  sltres  25540  sltsolem1  25544  dfrdg4  25711  frgra3vlem1  28112  frgra3vlem2  28113  frgrawopreg  28160  frgraregorufr  28164
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  df-3or 937  df-3an 938
  Copyright terms: Public domain W3C validator