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

Theorem 3jaodan 1279
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 1277 . 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 959
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 961  df-3an 962
This theorem is referenced by:  onzsl  6456  wemaplem2  7757  r1val1  7989  zeo  10723  xrltnsym  11110  xrlttri  11112  xrlttr  11113  qbtwnxr  11166  xltnegi  11182  xaddcom  11204  xnegdi  11207  xleadd1a  11212  xlt2add  11219  xsubge0  11220  xmullem  11223  xmulgt0  11242  xmulasslem3  11245  xlemul1a  11247  xadddilem  11253  xadddi  11254  xadddi2  11256  xrub  11270  isxmet2d  19861  blssioo  20331  icccvx  20481  ivthicc  20901  ismbf2d  21078  mbfmulc2lem  21084  itg2seq  21179  c1lip1  21428  dvivth  21441  reeff1o  21871  coseq00topi  21923  tanabsge  21927  logcnlem3  22048  atantan  22277  atanbnd  22280  cvxcl  22337  ostthlem1  22835  eliccioo  26039  xrpxdivcld  26043  esumcst  26450  3ccased  27304  lineelsb2  28108  bpoly3  28130  fnwe2lem3  29330
  Copyright terms: Public domain W3C validator