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

Theorem 3jaoi 1298
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 1170 . 2  |-  ( (
ph  ->  ps )  /\  ( ch  ->  ps )  /\  ( th  ->  ps ) )
5 3jao 1296 . 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 972    /\ w3a 973
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 704
This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975
This theorem is referenced by:  3jaoian  1300  3ianorr  1304  acexmidlem1  5849  nndceq  6478  nndcel  6479  znegcl  9243  xrltnr  9736  nltpnft  9771  ngtmnft  9774  xrrebnd  9776  xnegcl  9789  xnegneg  9790  xltnegi  9792  xrpnfdc  9799  xrmnfdc  9800  xnegid  9816  xaddid1  9819  xposdif  9839  prm23lt5  12217  zabsle1  13694
  Copyright terms: Public domain W3C validator