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

Theorem 3jaod 1236
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 1233 . 2  |-  ( ( ( ps  ->  ch )  /\  ( th  ->  ch )  /\  ( ta 
->  ch ) )  -> 
( ( ps  \/  th  \/  ta )  ->  ch ) )
51, 2, 3, 4syl3anc 1170 1  |-  ( ph  ->  ( ( ps  \/  th  \/  ta )  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ w3o 919
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663
This theorem depends on definitions:  df-bi 115  df-3or 921  df-3an 922
This theorem is referenced by:  3jaodan  1238  3jaao  1240  issod  4082  nnawordex  6167  addlocprlem  6787  nqprloc  6797  ltexprlemrl  6862  aptiprleml  6891  aptiprlemu  6892  elnn0z  8445  zaddcl  8472  zletric  8476  zlelttric  8477  zltnle  8478  zdceq  8504  zdcle  8505  zdclt  8506  nn01to3  8783  fzdcel  9135  qletric  9330  qlelttric  9331  qltnle  9332  qdceq  9333  frec2uzlt2d  9486
  Copyright terms: Public domain W3C validator