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

Theorem mpjao3dan 1319
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 798 . 2  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
4 mpjao3dan.3 . 2  |-  ( (
ph  /\  ta )  ->  ch )
5 mpjao3dan.4 . . 3  |-  ( ph  ->  ( ps  \/  th  \/  ta ) )
6 df-3or 981 . . 3  |-  ( ( ps  \/  th  \/  ta )  <->  ( ( ps  \/  th )  \/ 
ta ) )
75, 6sylib 122 . 2  |-  ( ph  ->  ( ( ps  \/  th )  \/  ta )
)
83, 4, 7mpjaodan 799 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    \/ wo 709    \/ w3o 979
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 710
This theorem depends on definitions:  df-bi 117  df-3or 981
This theorem is referenced by:  wetriext  4624  nntri3  6582  nntri2or2  6583  nntr2  6588  tridc  6995  nnnninfeq  7229  exmidontriimlem2  7333  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprprlemnkj  7804  caucvgprprlemnbj  7805  caucvgsr  7914  npnflt  9936  nmnfgt  9939  xleadd1a  9994  xltadd1  9997  xlt2add  10001  xsubge0  10002  xleaddadd  10008  addmodlteq  10541  iseqf1olemkle  10640  hashfiv01gt1  10925  iswrdiz  10999  xrmaxltsup  11540  xrmaxadd  11543  xrbdtri  11558  cvgratz  11814  zdvdsdc  12094  divalglemeunn  12203  divalglemex  12204  divalglemeuneg  12205  divalg  12206  znege1  12471  ennnfonelemk  12742  isxmet2d  14791  trilpolemres  15943  trirec0  15945
  Copyright terms: Public domain W3C validator