MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpjao3dan Structured version   Unicode version

Theorem mpjao3dan 1295
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 785 . 2  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
4 mpjao3dan.3 . 2  |-  ( (
ph  /\  ta )  ->  ch )
5 mpjao3dan.4 . . 3  |-  ( ph  ->  ( ps  \/  th  \/  ta ) )
6 df-3or 974 . . 3  |-  ( ( ps  \/  th  \/  ta )  <->  ( ( ps  \/  th )  \/ 
ta ) )
75, 6sylib 196 . 2  |-  ( ph  ->  ( ( ps  \/  th )  \/  ta )
)
83, 4, 7mpjaodan 786 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368    /\ wa 369    \/ w3o 972
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974
This theorem is referenced by:  wemaplem2  7990  r1val1  8221  xleadd1a  11470  xlt2add  11477  xmullem  11481  xmulgt0  11500  xmulasslem3  11503  xlemul1a  11505  xadddilem  11511  xadddi  11512  xadddi2  11514  isxmet2d  20955  icccvx  21575  ivthicc  21995  mbfmulc2lem  22179  c1lip1  22523  dvivth  22536  reeff1o  22967  coseq00topi  23020  tanabsge  23024  logcnlem3  23150  atantan  23379  atanbnd  23382  cvxcl  23439  ostthlem1  23937  tgdim01ln  24076  lnxfr  24078  lnext  24079  tgfscgr  24080  tglineeltr  24136  colmid  24190  xrpxdivcld  27783  archirngz  27885  archiabllem1b  27888  esumcst  28226  sgnmulsgn  28663  sgnmulsgp  28664  fnwe2lem3  31160
  Copyright terms: Public domain W3C validator