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  4636  onzsl  4637  tfrlem16  6409  oawordeulem  6552  elfiun  7183  domtriomlem  8068  axdc3lem2  8077  rankcf  8399  znegcl  10055  xrltnr  10462  xnegcl  10540  xnegneg  10541  xltnegi  10543  xnegid  10563  xaddid1  10566  xmulid1  10599  xrsupsslem  10625  xrinfmsslem  10626  ioombl1  18919  ppiublem1  20441  ostth  20788  kur14lem7  23743  3jaodd  24065  dfrdg2  24152  sltval2  24310  sltsgn1  24315  sltsgn2  24316  sltintdifex  24317  sltres  24318  sltsolem1  24322  dfrdg4  24488  fixpc  25094  fnckle  26045  pfsubkl  26047  gltpntl  26072  segline  26141  xsyysx  26145  nbssntrs  26147  pdiveql  26168  frgra3vlem1  28178  frgra3vlem2  28179
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