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

Theorem 3jaodan 1294
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 1292 . 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 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  df-3an 975
This theorem is referenced by:  onzsl  6659  wemaplem2  7968  r1val1  8200  zeo  10942  xrltnsym  11339  xrlttri  11341  xrlttr  11342  qbtwnxr  11395  xltnegi  11411  xaddcom  11433  xnegdi  11436  xleadd1a  11441  xlt2add  11448  xsubge0  11449  xmullem  11452  xmulgt0  11471  xmulasslem3  11474  xlemul1a  11476  xadddilem  11482  xadddi  11483  xadddi2  11485  xrub  11499  isxmet2d  20562  blssioo  21032  icccvx  21182  ivthicc  21602  ismbf2d  21780  mbfmulc2lem  21786  itg2seq  21881  c1lip1  22130  dvivth  22143  reeff1o  22573  coseq00topi  22625  tanabsge  22629  logcnlem3  22750  atantan  22979  atanbnd  22982  cvxcl  23039  ostthlem1  23537  eliccioo  27292  xrpxdivcld  27296  esumcst  27708  3ccased  28568  lineelsb2  29372  bpoly3  29394  fnwe2lem3  30602
  Copyright terms: Public domain W3C validator