Theorem jca32 520

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  reuan  3835  domssl  8942  domssr  8943  sbthlem9  9030  nqerf  10851  lemul12a  12011  lediv12a  12047  elfzd  13467  fzass4  13514  4fvwrd4  13600  leexp1a  14135  wrd2ind  14683  cshwidxm1  14767  rtrclreclem4  15021  coprmproddvdslem  16629  reumodprminv  16773  prmgaplem6  17025  mreexexlem2d  17609  sgrp2nmndlem4  18897  pmtrrn2  19433  rngcinv  20616  ringcinv  20650  islmodd  20863  nn0srg  21419  rge0srg  21420  mdet1  22591  cpmatmcllem  22708  neitr  23170  restnlly  23472  llyrest  23475  llyidm  23478  uptx  23615  alexsubALTlem2  24038  alexsubALTlem4  24040  distspace  24306  ncvs1  25149  ivthlem3  25445  conway  27796  uzsind  28422  renegscl  28515  readdscl  28516  remulscl  28519  axtg5seg  28558  colperpexlem3  28825  outpasch  28848  iscgra1  28903  f1otrg  28964  ax5seg  29032  axcontlem4  29061  eengtrkg  29080  wlkonwlk1l  29755  crctcshwlkn0  29914  wwlksnextinj  29992  wwlksnextsurj  29993  clwwlkf1  30144  clwwlknon1  30192  numclwwlk1lem2f1  30452  wlkl0  30462  grpoidinv  30604  pjnmopi  32244  cdj1i  32529  xrofsup  32866  ccfldsrarelvec  33862  dya2iocnrect  34472  omssubadd  34491  sitgfval  34532  bnj969  35135  bnj1463  35244  erdszelem7  35432  rellysconn  35486  segconeq  36245  ifscgr  36279  btwnconn1lem13  36334  btwnconn1lem14  36335  outsideofeq  36365  ellines  36387  fnessref  36592  refssfne  36593  knoppndvlem14  36838  isbasisrelowllem1  37724  isbasisrelowllem2  37725  relowlssretop  37732  itg2gt0cn  38049  frinfm  38109  heiborlem3  38187  isfldidl  38442  eldisjs6  39314  4atlem12  40111  cdleme48fv  40998  cdlemg35  41212  mapd0  42164  aks4d1p1p5  42567  flt4lem7  43116  nna4b4nsq  43117  3cubeslem1  43140  mzpincl  43190  mzpindd  43202  diophin  43228  pellexlem3  43283  pellexlem5  43285  dfno2  43879  amgm3d  44650  amgm4d  44651  lptre2pt  46090  dvnprodlem2  46397  stoweidlem1  46451  stoweidlem14  46464  stoweidlem17  46467  stoweidlem27  46477  stoweidlem57  46507  fourierdlem12  46569  fourierdlem14  46571  fourierdlem70  46626  fourierdlem92  46648  fourierdlem111  46667  etransclem10  46694  etransclem24  46708  salgenval  46771  smfaddlem1  47213  f1cof1blem  47544  elfzelfzlble  47791  reuopreuprim  48008  gpgedgvtx0  48559  rngcinvALTV  48774  ringcinvALTV  48808  lmod1  48990  inlinecirc02plem  49284  nelsubclem  49564  oppf1st2nd  49628