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

Theorem mpjao3dan 1243
Description: Eliminate a 3-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.)
Hypotheses
Ref Expression
mpjao3dan.1  |-  ( (
ph  /\  ps )  ->  ch )
mpjao3dan.2  |-  ( (
ph  /\  th )  ->  ch )
mpjao3dan.3  |-  ( (
ph  /\  ta )  ->  ch )
mpjao3dan.4  |-  ( ph  ->  ( ps  \/  th  \/  ta ) )
Assertion
Ref Expression
mpjao3dan  |-  ( ph  ->  ch )

Proof of Theorem mpjao3dan
StepHypRef Expression
1 mpjao3dan.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
2 mpjao3dan.2 . . 3  |-  ( (
ph  /\  th )  ->  ch )
31, 2jaodan 746 . 2  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
4 mpjao3dan.3 . 2  |-  ( (
ph  /\  ta )  ->  ch )
5 mpjao3dan.4 . . 3  |-  ( ph  ->  ( ps  \/  th  \/  ta ) )
6 df-3or 925 . . 3  |-  ( ( ps  \/  th  \/  ta )  <->  ( ( ps  \/  th )  \/ 
ta ) )
75, 6sylib 120 . 2  |-  ( ph  ->  ( ( ps  \/  th )  \/  ta )
)
83, 4, 7mpjaodan 747 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    \/ wo 664    \/ w3o 923
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 665
This theorem depends on definitions:  df-bi 115  df-3or 925
This theorem is referenced by:  wetriext  4392  nntri3  6258  nntri2or2  6259  tridc  6613  caucvgprlemnkj  7223  caucvgprlemnbj  7224  caucvgprprlemnkj  7249  caucvgprprlemnbj  7250  caucvgsr  7345  addmodlteq  9801  iseqf1olemkle  9909  hashfiv01gt1  10186  cvgratz  10922  zdvdsdc  11091  divalglemeunn  11195  divalglemex  11196  divalglemeuneg  11197  divalg  11198  znege1  11430  nninfalllemn  11853
  Copyright terms: Public domain W3C validator