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  4578  nntri3  6500  nntri2or2  6501  nntr2  6506  tridc  6901  nnnninfeq  7128  exmidontriimlem2  7223  caucvgprlemnkj  7667  caucvgprlemnbj  7668  caucvgprprlemnkj  7693  caucvgprprlemnbj  7694  caucvgsr  7803  npnflt  9817  nmnfgt  9820  xleadd1a  9875  xltadd1  9878  xlt2add  9882  xsubge0  9883  xleaddadd  9889  addmodlteq  10400  iseqf1olemkle  10486  hashfiv01gt1  10764  xrmaxltsup  11268  xrmaxadd  11271  xrbdtri  11286  cvgratz  11542  zdvdsdc  11821  divalglemeunn  11928  divalglemex  11929  divalglemeuneg  11930  divalg  11931  znege1  12180  ennnfonelemk  12403  isxmet2d  13933  trilpolemres  14875  trirec0  14877
  Copyright terms: Public domain W3C validator