ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3jaoi Unicode version

Theorem 3jaoi 1303
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 1175 . 2  |-  ( (
ph  ->  ps )  /\  ( ch  ->  ps )  /\  ( th  ->  ps ) )
5 3jao 1301 . 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 977    /\ w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709
This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980
This theorem is referenced by:  3jaoian  1305  3ianorr  1309  acexmidlem1  5870  nndceq  6499  nndcel  6500  znegcl  9283  xrltnr  9778  nltpnft  9813  ngtmnft  9816  xrrebnd  9818  xnegcl  9831  xnegneg  9832  xltnegi  9834  xrpnfdc  9841  xrmnfdc  9842  xnegid  9858  xaddid1  9861  xposdif  9881  prm23lt5  12262  zabsle1  14370
  Copyright terms: Public domain W3C validator