Theorem jca32 508

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 504	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5	1, 4	jca 504	1 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  syl12anc  824  reuan  3784  sbthlem9  8431  nqerf  10150  lemul12a  11299  lediv12a  11334  fzass4  12761  4fvwrd4  12843  leexp1a  13354  wrd2ind  13917  wrd2indOLD  13918  cshwidxm1  14031  rtrclreclem4  14281  coprmproddvdslem  15862  reumodprminv  15997  prmgaplem6  16248  mreexexlem2d  16774  sgrp2nmndlem4  17884  pmtrrn2  18349  islmodd  19362  nn0srg  20317  rge0srg  20318  mdet1  20914  cpmatmcllem  21030  neitr  21492  restnlly  21794  llyrest  21797  llyidm  21800  uptx  21937  alexsubALTlem2  22360  alexsubALTlem4  22362  distspace  22629  ncvs1  23464  ivthlem3  23757  axtg5seg  25953  colperpexlem3  26220  outpasch  26243  iscgra1  26298  f1otrg  26360  ax5seg  26427  axcontlem4  26456  eengtrkg  26475  wlkonwlk1l  27147  crctcshwlkn0  27307  wwlksnextinj  27390  wwlksnextsurj  27391  wwlksnextinjOLD  27395  wwlksnextsurOLD  27396  clwwlkf1OLD  27566  clwwlkf1  27571  clwwlknon1  27625  numclwwlk1lem2f1  27899  numclwwlk1lem2f1OLD  27904  wlkl0  27920  grpoidinv  28062  pjnmopi  29706  cdj1i  29991  xrofsup  30244  ccfldsrarelvec  30682  dya2iocnrect  31181  omssubadd  31200  sitgfval  31241  bnj969  31862  bnj1463  31969  erdszelem7  32026  rellysconn  32080  conway  32782  etasslt  32792  segconeq  32989  ifscgr  33023  btwnconn1lem13  33078  btwnconn1lem14  33079  outsideofeq  33109  ellines  33131  fnessref  33223  refssfne  33224  knoppndvlem14  33381  isbasisrelowllem1  34075  isbasisrelowllem2  34076  relowlssretop  34083  itg2gt0cn  34385  frinfm  34449  heiborlem3  34530  isfldidl  34785  4atlem12  36190  cdleme48fv  37077  cdlemg35  37291  mapd0  38243  mzpincl  38723  mzpindd  38735  diophin  38762  pellexlem3  38821  pellexlem5  38823  amgm3d  39914  amgm4d  39915  monoords  40991  uzfissfz  41021  iuneqfzuzlem  41029  ssuzfz  41044  elfzd  41112  mccllem  41307  sumnnodd  41340  lptre2pt  41350  dvnmul  41656  dvnprodlem1  41659  dvnprodlem2  41660  itgspltprt  41692  stoweidlem1  41715  stoweidlem3  41717  stoweidlem14  41728  stoweidlem17  41731  stoweidlem27  41741  stoweidlem57  41771  fourierdlem12  41833  fourierdlem14  41835  fourierdlem41  41862  fourierdlem48  41868  fourierdlem49  41869  fourierdlem50  41870  fourierdlem70  41890  fourierdlem79  41899  fourierdlem92  41912  fourierdlem111  41931  elaa2lem  41947  etransclem3  41951  etransclem7  41955  etransclem10  41958  etransclem24  41972  etransclem27  41975  etransclem28  41976  etransclem35  41983  etransclem38  41986  etransclem44  41992  salgenval  42035  iundjiun  42171  caratheodorylem1  42237  smfaddlem1  42468  elfzelfzlble  42925  reuopreuprim  43054  rngcinv  43614  rngcinvALTV  43626  ringcinv  43665  lmod1  43912  inlinecirc02plem  44139