MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3jaodan Structured version   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  4826  wemaplem2  7516  r1val1  7712  zeo  10355  xrltnsym  10730  xrlttri  10732  xrlttr  10733  qbtwnxr  10786  xltnegi  10802  xaddcom  10824  xnegdi  10827  xleadd1a  10832  xlt2add  10839  xsubge0  10840  xmullem  10843  xmulgt0  10862  xmulasslem3  10865  xlemul1a  10867  xadddilem  10873  xadddi  10874  xadddi2  10876  xrub  10890  isxmet2d  18357  blssioo  18826  icccvx  18975  ivthicc  19355  ismbf2d  19533  mbfmulc2lem  19539  itg2seq  19634  c1lip1  19881  dvivth  19894  reeff1o  20363  coseq00topi  20410  tanabsge  20414  logcnlem3  20535  atantan  20763  atanbnd  20766  cvxcl  20823  ostthlem1  21321  eliccioo  24177  xrpxdivcld  24181  esumcst  24455  3ccased  25176  lineelsb2  26082  bpoly3  26104  fnwe2lem3  27127
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