Theorem jca32 523

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  reuan  3847  domssl  8972  domssr  8973  sbthlem9  9060  nqerf  10881  lemul12a  12042  lediv12a  12078  elfzd  13513  fzass4  13560  4fvwrd4  13646  leexp1a  14181  wrd2ind  14729  cshwidxm1  14813  rtrclreclem4  15067  coprmproddvdslem  16686  reumodprminv  16830  prmgaplem6  17082  mreexexlem2d  17667  sgrp2nmndlem4  18955  pmtrrn2  19490  rngcinv  20673  ringcinv  20707  islmodd  20920  nn0srg  21476  rge0srg  21477  mdet1  22648  cpmatmcllem  22765  neitr  23227  restnlly  23529  llyrest  23532  llyidm  23535  uptx  23672  alexsubALTlem2  24095  alexsubALTlem4  24097  distspace  24363  ncvs1  25206  ivthlem3  25502  conway  27859  uzsind  28485  renegscl  28578  readdscl  28579  remulscl  28582  axtg5seg  28621  colperpexlem3  28888  outpasch  28911  iscgra1  28966  f1otrg  29027  ax5seg  29095  axcontlem4  29124  eengtrkg  29143  wlkonwlk1l  29818  crctcshwlkn0  29977  wwlksnextinj  30055  wwlksnextsurj  30056  clwwlkf1  30207  clwwlknon1  30255  numclwwlk1lem2f1  30515  wlkl0  30525  grpoidinv  30667  pjnmopi  32307  cdj1i  32592  xrofsup  32929  ccfldsrarelvec  33928  dya2iocnrect  34538  omssubadd  34557  sitgfval  34598  bnj969  35201  bnj1463  35310  erdszelem7  35507  rellysconn  35561  segconeq  36320  ifscgr  36354  btwnconn1lem13  36409  btwnconn1lem14  36410  outsideofeq  36440  ellines  36462  fnessref  36677  refssfne  36678  knoppndvlem14  36923  isbasisrelowllem1  37809  isbasisrelowllem2  37810  relowlssretop  37817  itg2gt0cn  38134  frinfm  38194  heiborlem3  38272  isfldidl  38527  eldisjs6  39399  4atlem12  40196  cdleme48fv  41083  cdlemg35  41297  mapd0  42249  aks4d1p1p5  42652  flt4lem7  43201  nna4b4nsq  43202  3cubeslem1  43225  mzpincl  43275  mzpindd  43287  diophin  43313  pellexlem3  43368  pellexlem5  43370  dfno2  43964  amgm3d  44735  amgm4d  44736  lptre2pt  46174  dvnprodlem2  46481  stoweidlem1  46535  stoweidlem14  46548  stoweidlem17  46551  stoweidlem27  46561  stoweidlem57  46591  fourierdlem12  46653  fourierdlem14  46655  fourierdlem70  46710  fourierdlem92  46732  fourierdlem111  46751  etransclem10  46778  etransclem24  46792  salgenval  46855  smfaddlem1  47297  f1cof1blem  47628  elfzelfzlble  47875  reuopreuprim  48092  gpgedgvtx0  48643  rngcinvALTV  48858  ringcinvALTV  48892  lmod1  49074  inlinecirc02plem  49368  nelsubclem  49648  oppf1st2nd  49712