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

Theorem 3jaodan 1250
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 424 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 3jaodan.2 . . . 4  |-  ( (
ph  /\  th )  ->  ch )
43ex 424 . . 3  |-  ( ph  ->  ( th  ->  ch ) )
5 3jaodan.3 . . . 4  |-  ( (
ph  /\  ta )  ->  ch )
65ex 424 . . 3  |-  ( ph  ->  ( ta  ->  ch ) )
72, 4, 63jaod 1248 . 2  |-  ( ph  ->  ( ( ps  \/  th  \/  ta )  ->  ch ) )
87imp 419 1  |-  ( (
ph  /\  ( ps  \/  th  \/  ta )
)  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    \/ w3o 935
This theorem is referenced by:  onzsl  4785  wemaplem2  7472  r1val1  7668  zeo  10311  xrltnsym  10686  xrlttri  10688  xrlttr  10689  qbtwnxr  10742  xltnegi  10758  xaddcom  10780  xnegdi  10783  xleadd1a  10788  xlt2add  10795  xsubge0  10796  xmullem  10799  xmulgt0  10818  xmulasslem3  10821  xlemul1a  10823  xadddilem  10829  xadddi  10830  xadddi2  10832  xrub  10846  isxmet2d  18310  blssioo  18779  icccvx  18928  ivthicc  19308  ismbf2d  19486  mbfmulc2lem  19492  itg2seq  19587  c1lip1  19834  dvivth  19847  reeff1o  20316  coseq00topi  20363  tanabsge  20367  logcnlem3  20488  atantan  20716  atanbnd  20719  cvxcl  20776  ostthlem1  21274  eliccioo  24130  xrpxdivcld  24134  esumcst  24408  3ccased  25129  lineelsb2  25986  bpoly3  26008  fnwe2lem3  27017
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938
  Copyright terms: Public domain W3C validator