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

Theorem jca31 534
Description: Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.)
Hypotheses
Ref Expression
jca31.1
jca31.2
jca31.3
Assertion
Ref Expression
jca31

Proof of Theorem jca31
StepHypRef Expression
1 jca31.1 . . 3
2 jca31.2 . . 3
31, 2jca 532 . 2
4 jca31.3 . 2
53, 4jca 532 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  3jca  1176  syl21anc  1227  xpdifid  5440  f1oiso2  6248  oewordri  7260  boxriin  7531  cantnfrescl  8116  cfsuc  8658  genpcl  9407  ltexprlem5  9439  prsrlem1  9470  lemulge11  10429  lediv12a  10463  elnnz  10899  uzindOLD  10982  quoremz  11982  quoremnn0ALT  11984  fldiv  11987  leexp1a  12224  faclbnd6  12377  wrdlen2i  12884  wwlktovfo  12896  setcinv  15417  sgrp2rid2  16044  mhmfmhm  16193  gsumval3lem1  16909  dvdsrzring  18507  dvdsrz  18508  scmatmhm  19036  cncnp2  19782  vitalilem1  22017  aaliou3lem2  22739  pntibndlem2  23776  oppcom  24116  opphllem1  24119  opphllem2  24120  opphllem5  24123  hpgerlem  24134  ax5seg  24241  constr3lem4  24647  wlknwwlknsur  24712  wlkiswwlksur  24719  frgrancvvdeqlem4  25033  usg2spot2nb  25065  grpoidinv  25210  isrngod  25381  nmcvcn  25605  leopmul  27053  resf1o  27553  rhmopp  27809  oddpwdc  28293  poseq  29333  btwnconn1  29751  finminlem  30136  lzenom  30703  jm2.27c  30949  mullimc  31622  mullimcf  31629  addlimc  31654  0ellimcdiv  31655  cncfshift  31676  cncfperiod  31681  icccncfext  31690  stoweidlem52  31834  wallispilem4  31850  fourierdlem16  31905  fourierdlem21  31910  fourierdlem48  31937  fourierdlem51  31940  fourierdlem52  31941  fourierdlem54  31943  fourierdlem64  31953  fourierdlem76  31965  fourierdlem77  31966  fourierdlem80  31969  fourierdlem86  31975  fourierdlem87  31976  fourierdlem102  31991  fourierdlem114  32003  usgra2pthlem1  32353  tpres  32554  rngcinv  32789  rngcinvOLD  32801  ringcinv  32840  ringcinvOLD  32864  2pm13.193  33325  bj-elid3  34601  paddasslem4  35547  cdleme21h  36060  cdleme26eALTN  36087  cdleme40m  36193  cdlemf2  36288  dicssdvh  36913  dihopelvalcpre  36975  dihmeetlem4preN  37033  dih1dimatlem0  37055
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-an 371
  Copyright terms: Public domain W3C validator