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  4784  onzsl  4785  tfrlem16  6613  oawordeulem  6756  elfiun  7393  domtriomlem  8278  axdc3lem2  8287  rankcf  8608  znegcl  10269  xrltnr  10676  xnegcl  10755  xnegneg  10756  xltnegi  10758  xnegid  10778  xaddid1  10781  xmulid1  10814  xrsupsslem  10841  xrinfmsslem  10842  elfznelfzo  11147  hashtpg  11646  ioombl1  19409  ppiublem1  20939  ostth  21286  nb3graprlem1  21413  kur14lem7  24851  3jaodd  25121  dfrdg2  25366  sltval2  25524  sltsgn1  25529  sltsgn2  25530  sltintdifex  25531  sltres  25532  sltsolem1  25536  dfrdg4  25703  frgra3vlem1  28104  frgra3vlem2  28105  frgrawopreg  28152  frgraregorufr  28156
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