Theorem jca32 535

Description: Join three consequents. (Contributed by FL, 1-Aug-2009.)

Hypotheses

Ref	Expression
jca31.1
jca31.2
jca31.3

Assertion

Ref	Expression
jca32

Proof of Theorem jca32

Step	Hyp	Ref	Expression
1		jca31.1	. 2
2		jca31.2	. . 3
3		jca31.3	. . 3
4	2, 3	jca 532	. 2
5	1, 4	jca 532	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  syl12anc  1226  sbthlem9  7655  nqerf  9329  lemul12a  10425  lediv12a  10463  fzass4  11750  elfz1b  11777  4fvwrd4  11822  leexp1a  12224  wrd2ind  12703  cshwidxm1  12777  mreexexlem2d  15042  sgrp2nmndlem4  16046  pmtrrn2  16485  islmodd  17518  nn0srg  18486  rge0srg  18487  mdet1  19103  cpmatmcllem  19219  istps2OLD  19422  neitr  19681  restnlly  19983  llyrest  19986  llyidm  19989  uptx  20126  alexsubALTlem2  20548  alexsubALTlem4  20550  ivthlem3  21865  axtg5seg  23862  colperpexlem3  24106  f1otrg  24174  ax5seg  24241  axcontlem4  24270  eengtrkg  24288  wwlkextinj  24730  wwlkextsur  24731  clwwlkf1  24796  usg2spot2nb  25065  grpoidinv  25210  pjnmopi  27067  cdj1i  27352  xrofsup  27582  dya2iocnrect  28252  sitgfval  28283  erdszelem7  28641  rellyscon  28696  relexpadd  29061  rtrclreclem.min  29070  segconeq  29660  ifscgr  29694  btwnconn1lem13  29749  btwnconn1lem14  29750  outsideofeq  29780  ellines  29802  itg2gt0cn  30070  fnessref  30175  refssfne  30176  frinfm  30226  heiborlem3  30309  isfldidl  30465  mzpincl  30666  mzpindd  30678  diophin  30706  pellexlem3  30767  pellexlem5  30769  monoords  31496  mccllem  31605  sumnnodd  31636  lptre2pt  31646  dvnmul  31740  dvnprodlem1  31743  dvnprodlem2  31744  itgspltprt  31778  stoweidlem1  31783  stoweidlem3  31785  stoweidlem14  31796  stoweidlem17  31799  stoweidlem27  31809  stoweidlem57  31839  fourierdlem12  31901  fourierdlem14  31903  fourierdlem41  31930  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem70  31959  fourierdlem79  31968  fourierdlem92  31981  fourierdlem111  32000  elaa2lem  32016  etransclem3  32020  etransclem7  32024  etransclem10  32027  etransclem24  32041  etransclem27  32044  etransclem28  32045  etransclem35  32052  etransclem38  32055  etransclem44  32061  reuan  32185  elfzelfzlble  32337  rngcinv  32789  rngcinvOLD  32801  ringcinv  32840  lmod1  33093  bnj969  34004  bnj1463  34111  4atlem12  35336  cdleme48fv  36225  cdlemg35  36439  mapd0  37392

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