Theorem jca32 515

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  reuan  3848  domssl  8947  domssr  8948  sbthlem9  9035  nqerf  10853  lemul12a  12011  lediv12a  12047  elfzd  13443  fzass4  13490  4fvwrd4  13576  leexp1a  14110  wrd2ind  14658  cshwidxm1  14742  rtrclreclem4  14996  coprmproddvdslem  16601  reumodprminv  16744  prmgaplem6  16996  mreexexlem2d  17580  sgrp2nmndlem4  18865  pmtrrn2  19401  rngcinv  20582  ringcinv  20616  islmodd  20829  nn0srg  21404  rge0srg  21405  mdet1  22557  cpmatmcllem  22674  neitr  23136  restnlly  23438  llyrest  23441  llyidm  23444  uptx  23581  alexsubALTlem2  24004  alexsubALTlem4  24006  distspace  24272  ncvs1  25125  ivthlem3  25422  conway  27787  uzsind  28413  renegscl  28506  readdscl  28507  remulscl  28510  axtg5seg  28549  colperpexlem3  28816  outpasch  28839  iscgra1  28894  f1otrg  28955  ax5seg  29023  axcontlem4  29052  eengtrkg  29071  wlkonwlk1l  29747  crctcshwlkn0  29906  wwlksnextinj  29984  wwlksnextsurj  29985  clwwlkf1  30136  clwwlknon1  30184  numclwwlk1lem2f1  30444  wlkl0  30454  grpoidinv  30595  pjnmopi  32235  cdj1i  32520  xrofsup  32857  ccfldsrarelvec  33848  dya2iocnrect  34458  omssubadd  34477  sitgfval  34518  bnj969  35121  bnj1463  35230  erdszelem7  35410  rellysconn  35464  segconeq  36223  ifscgr  36257  btwnconn1lem13  36312  btwnconn1lem14  36313  outsideofeq  36343  ellines  36365  fnessref  36570  refssfne  36571  knoppndvlem14  36744  isbasisrelowllem1  37607  isbasisrelowllem2  37608  relowlssretop  37615  itg2gt0cn  37923  frinfm  37983  heiborlem3  38061  isfldidl  38316  eldisjs6  39188  4atlem12  39985  cdleme48fv  40872  cdlemg35  41086  mapd0  42038  aks4d1p1p5  42442  flt4lem7  43014  nna4b4nsq  43015  3cubeslem1  43038  mzpincl  43088  mzpindd  43100  diophin  43126  pellexlem3  43185  pellexlem5  43187  dfno2  43781  amgm3d  44552  amgm4d  44553  lptre2pt  45995  dvnprodlem2  46302  stoweidlem1  46356  stoweidlem14  46369  stoweidlem17  46372  stoweidlem27  46382  stoweidlem57  46412  fourierdlem12  46474  fourierdlem14  46476  fourierdlem70  46531  fourierdlem92  46553  fourierdlem111  46572  etransclem10  46599  etransclem24  46613  salgenval  46676  smfaddlem1  47118  f1cof1blem  47431  elfzelfzlble  47678  reuopreuprim  47883  gpgedgvtx0  48418  rngcinvALTV  48633  ringcinvALTV  48667  lmod1  48849  inlinecirc02plem  49143  nelsubclem  49423  oppf1st2nd  49487