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

Theorem 3jaoi 1248
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 1133 . 2  |-  ( (
ph  ->  ps )  /\  ( ch  ->  ps )  /\  ( th  ->  ps ) )
5 3jao 1246 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ch  ->  ps )  /\  ( th 
->  ps ) )  -> 
( ( ph  \/  ch  \/  th )  ->  ps ) )
64, 5ax-mp 5 1  |-  ( (
ph  \/  ch  \/  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ w3o 936    /\ w3a 937
This theorem is referenced by:  3jaoian  1250  ordzsl  4828  onzsl  4829  tfrlem16  6657  oawordeulem  6800  elfiun  7438  domtriomlem  8327  axdc3lem2  8336  rankcf  8657  znegcl  10318  xrltnr  10725  xnegcl  10804  xnegneg  10805  xltnegi  10807  xnegid  10827  xaddid1  10830  xmulid1  10863  xrsupsslem  10890  xrinfmsslem  10891  elfznelfzo  11197  hashtpg  11696  ioombl1  19461  ppiublem1  20991  ostth  21338  nb3graprlem1  21465  kur14lem7  24903  3jaodd  25173  dfrdg2  25428  sltval2  25616  sltsgn1  25621  sltsgn2  25622  sltintdifex  25623  sltres  25624  sltsolem1  25628  dfrdg4  25800  wl-exeq  26239  cshwssizelem3  28316  frgra3vlem1  28464  frgra3vlem2  28465  frgrawopreg  28512  frgraregorufr  28516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939
  Copyright terms: Public domain W3C validator