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

Theorem 3jaodan 1285
Description: Disjunction of 3 antecedents (deduction). (Contributed by NM, 14-Oct-2005.)
Hypotheses
Ref Expression
3jaodan.1  |-  ( (
ph  /\  ps )  ->  ch )
3jaodan.2  |-  ( (
ph  /\  th )  ->  ch )
3jaodan.3  |-  ( (
ph  /\  ta )  ->  ch )
Assertion
Ref Expression
3jaodan  |-  ( (
ph  /\  ( ps  \/  th  \/  ta )
)  ->  ch )

Proof of Theorem 3jaodan
StepHypRef Expression
1 3jaodan.1 . . . 4  |-  ( (
ph  /\  ps )  ->  ch )
21ex 434 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 3jaodan.2 . . . 4  |-  ( (
ph  /\  th )  ->  ch )
43ex 434 . . 3  |-  ( ph  ->  ( th  ->  ch ) )
5 3jaodan.3 . . . 4  |-  ( (
ph  /\  ta )  ->  ch )
65ex 434 . . 3  |-  ( ph  ->  ( ta  ->  ch ) )
72, 4, 63jaod 1283 . 2  |-  ( ph  ->  ( ( ps  \/  th  \/  ta )  ->  ch ) )
87imp 429 1  |-  ( (
ph  /\  ( ps  \/  th  \/  ta )
)  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    \/ w3o 964
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 966  df-3an 967
This theorem is referenced by:  onzsl  6562  wemaplem2  7867  r1val1  8099  zeo  10833  xrltnsym  11220  xrlttri  11222  xrlttr  11223  qbtwnxr  11276  xltnegi  11292  xaddcom  11314  xnegdi  11317  xleadd1a  11322  xlt2add  11329  xsubge0  11330  xmullem  11333  xmulgt0  11352  xmulasslem3  11355  xlemul1a  11357  xadddilem  11363  xadddi  11364  xadddi2  11366  xrub  11380  isxmet2d  20029  blssioo  20499  icccvx  20649  ivthicc  21069  ismbf2d  21247  mbfmulc2lem  21253  itg2seq  21348  c1lip1  21597  dvivth  21610  reeff1o  22040  coseq00topi  22092  tanabsge  22096  logcnlem3  22217  atantan  22446  atanbnd  22449  cvxcl  22506  ostthlem1  23004  eliccioo  26246  xrpxdivcld  26250  esumcst  26654  3ccased  27514  lineelsb2  28318  bpoly3  28340  fnwe2lem3  29548
  Copyright terms: Public domain W3C validator