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  4637  wemaplem2  7262  r1val1  7458  zeo  10097  xrltnsym  10471  xrlttri  10473  xrlttr  10474  qbtwnxr  10527  xltnegi  10543  xaddcom  10565  xnegdi  10568  xleadd1a  10573  xlt2add  10580  xsubge0  10581  xmullem  10584  xmulgt0  10603  xmulasslem3  10606  xlemul1a  10608  xadddilem  10614  xadddi  10615  xadddi2  10617  xrub  10630  isxmet2d  17892  blssioo  18301  icccvx  18448  ivthicc  18818  ismbf2d  18996  mbfmulc2lem  19002  itg2seq  19097  c1lip1  19344  dvivth  19357  reeff1o  19823  coseq00topi  19870  tanabsge  19874  logcnlem3  19991  atantan  20219  atanbnd  20222  cvxcl  20279  ostthlem1  20776  eliccioo  23115  xrpxdivcld  23119  esumcst  23436  3ccased  24073  lineelsb2  24771  bpoly3  24793  fnwe2lem3  27149
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