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

Theorem 3jaodan 1248
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 423 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 3jaodan.2 . . . 4  |-  ( (
ph  /\  th )  ->  ch )
43ex 423 . . 3  |-  ( ph  ->  ( th  ->  ch ) )
5 3jaodan.3 . . . 4  |-  ( (
ph  /\  ta )  ->  ch )
65ex 423 . . 3  |-  ( ph  ->  ( ta  ->  ch ) )
72, 4, 63jaod 1246 . 2  |-  ( ph  ->  ( ( ps  \/  th  \/  ta )  ->  ch ) )
87imp 418 1  |-  ( (
ph  /\  ( ps  \/  th  \/  ta )
)  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    \/ w3o 933
This theorem is referenced by:  onzsl  4653  wemaplem2  7278  r1val1  7474  zeo  10113  xrltnsym  10487  xrlttri  10489  xrlttr  10490  qbtwnxr  10543  xltnegi  10559  xaddcom  10581  xnegdi  10584  xleadd1a  10589  xlt2add  10596  xsubge0  10597  xmullem  10600  xmulgt0  10619  xmulasslem3  10622  xlemul1a  10624  xadddilem  10630  xadddi  10631  xadddi2  10633  xrub  10646  isxmet2d  17908  blssioo  18317  icccvx  18464  ivthicc  18834  ismbf2d  19012  mbfmulc2lem  19018  itg2seq  19113  c1lip1  19360  dvivth  19373  reeff1o  19839  coseq00topi  19886  tanabsge  19890  logcnlem3  20007  atantan  20235  atanbnd  20238  cvxcl  20295  ostthlem1  20792  eliccioo  23131  xrpxdivcld  23135  esumcst  23451  3ccased  24088  lineelsb2  24843  bpoly3  24865  fnwe2lem3  27252
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 177  df-or 359  df-an 360  df-3or 935  df-3an 936
  Copyright terms: Public domain W3C validator