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

Theorem 3jaoi 1245
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 1130 . 2  |-  ( (
ph  ->  ps )  /\  ( ch  ->  ps )  /\  ( th  ->  ps ) )
5 3jao 1243 . 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 933    /\ w3a 934
This theorem is referenced by:  3jaoian  1247  ordzsl  4652  onzsl  4653  tfrlem16  6425  oawordeulem  6568  elfiun  7199  domtriomlem  8084  axdc3lem2  8093  rankcf  8415  znegcl  10071  xrltnr  10478  xnegcl  10556  xnegneg  10557  xltnegi  10559  xnegid  10579  xaddid1  10582  xmulid1  10615  xrsupsslem  10641  xrinfmsslem  10642  ioombl1  18935  ppiublem1  20457  ostth  20804  kur14lem7  23758  3jaodd  24080  dfrdg2  24223  sltval2  24381  sltsgn1  24386  sltsgn2  24387  sltintdifex  24388  sltres  24389  sltsolem1  24393  dfrdg4  24560  itg2addnclem  25003  fixpc  25197  fnckle  26148  pfsubkl  26150  gltpntl  26175  segline  26244  xsyysx  26248  nbssntrs  26250  pdiveql  26271  elfznelfzo  28213  hashtpg  28217  nb3graprlem1  28287  frgra3vlem1  28424  frgra3vlem2  28425
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  df-3or 935  df-3an 936
  Copyright terms: Public domain W3C validator