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

Theorem 3jaoi 1285
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 1160 . 2  |-  ( (
ph  ->  ps )  /\  ( ch  ->  ps )  /\  ( th  ->  ps ) )
5 3jao 1283 . 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 962    /\ w3a 963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699
This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965
This theorem is referenced by:  3jaoian  1287  3ianorr  1291  acexmidlem1  5821  nndceq  6447  nndcel  6448  znegcl  9199  xrltnr  9687  nltpnft  9719  ngtmnft  9722  xrrebnd  9724  xnegcl  9737  xnegneg  9738  xltnegi  9740  xrpnfdc  9747  xrmnfdc  9748  xnegid  9764  xaddid1  9767  xposdif  9787  prm23lt5  12142
  Copyright terms: Public domain W3C validator