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

Theorem 3jaod 1282
Description: Disjunction of 3 antecedents (deduction). (Contributed by NM, 14-Oct-2005.)
Hypotheses
Ref Expression
3jaod.1  |-  ( ph  ->  ( ps  ->  ch ) )
3jaod.2  |-  ( ph  ->  ( th  ->  ch ) )
3jaod.3  |-  ( ph  ->  ( ta  ->  ch ) )
Assertion
Ref Expression
3jaod  |-  ( ph  ->  ( ( ps  \/  th  \/  ta )  ->  ch ) )

Proof of Theorem 3jaod
StepHypRef Expression
1 3jaod.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 3jaod.2 . 2  |-  ( ph  ->  ( th  ->  ch ) )
3 3jaod.3 . 2  |-  ( ph  ->  ( ta  ->  ch ) )
4 3jao 1279 . 2  |-  ( ( ( ps  ->  ch )  /\  ( th  ->  ch )  /\  ( ta 
->  ch ) )  -> 
( ( ps  \/  th  \/  ta )  ->  ch ) )
51, 2, 3, 4syl3anc 1216 1  |-  ( ph  ->  ( ( ps  \/  th  \/  ta )  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ w3o 961
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 698
This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964
This theorem is referenced by:  3jaodan  1284  3jaao  1286  issod  4236  nnawordex  6417  addlocprlem  7336  nqprloc  7346  ltexprlemrl  7411  aptiprleml  7440  aptiprlemu  7441  elnn0z  9060  zaddcl  9087  zletric  9091  zlelttric  9092  zltnle  9093  zdceq  9119  zdcle  9120  zdclt  9121  nn01to3  9402  xposdif  9658  fzdcel  9813  qletric  10014  qlelttric  10015  qltnle  10016  qdceq  10017  frec2uzlt2d  10170  triap  13209
  Copyright terms: Public domain W3C validator