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

Theorem mpjao3dan 1307
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 797 . 2  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
4 mpjao3dan.3 . 2  |-  ( (
ph  /\  ta )  ->  ch )
5 mpjao3dan.4 . . 3  |-  ( ph  ->  ( ps  \/  th  \/  ta ) )
6 df-3or 979 . . 3  |-  ( ( ps  \/  th  \/  ta )  <->  ( ( ps  \/  th )  \/ 
ta ) )
75, 6sylib 122 . 2  |-  ( ph  ->  ( ( ps  \/  th )  \/  ta )
)
83, 4, 7mpjaodan 798 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    \/ wo 708    \/ w3o 977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709
This theorem depends on definitions:  df-bi 117  df-3or 979
This theorem is referenced by:  wetriext  4576  nntri3  6497  nntri2or2  6498  nntr2  6503  tridc  6898  nnnninfeq  7125  exmidontriimlem2  7220  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprprlemnkj  7690  caucvgprprlemnbj  7691  caucvgsr  7800  npnflt  9813  nmnfgt  9816  xleadd1a  9871  xltadd1  9874  xlt2add  9878  xsubge0  9879  xleaddadd  9885  addmodlteq  10395  iseqf1olemkle  10481  hashfiv01gt1  10757  xrmaxltsup  11261  xrmaxadd  11264  xrbdtri  11279  cvgratz  11535  zdvdsdc  11814  divalglemeunn  11920  divalglemex  11921  divalglemeuneg  11922  divalg  11923  znege1  12172  ennnfonelemk  12395  isxmet2d  13741  trilpolemres  14672  trirec0  14674
  Copyright terms: Public domain W3C validator