Theorem jca32 524

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  reuan  3851  domssl  8996  domssr  8997  sbthlem9  9084  nqerf  10916  lemul12a  12074  lediv12a  12109  elfzd  13544  fzass4  13592  4fvwrd4  13678  leexp1a  14213  wrd2ind  14762  cshwidxm1  14846  rtrclreclem4  15100  coprmproddvdslem  16721  reumodprminv  16865  prmgaplem6  17117  mreexexlem2d  17702  sgrp2nmndlem4  18991  pmtrrn2  19531  rngcinv  20723  ringcinv  20757  islmodd  20968  nn0srg  21568  rge0srg  21569  mdet1  22739  cpmatmcllem  22856  neitr  23318  restnlly  23620  llyrest  23623  llyidm  23626  uptx  23763  alexsubALTlem2  24186  alexsubALTlem4  24188  distspace  24454  ncvs1  25297  ivthlem3  25593  conway  27953  uzsind  28579  renegscl  28672  readdscl  28673  remulscl  28676  axtg5seg  28715  tglnpt3  28908  colperpexlem3  28994  outpasch  29018  iscgra1  29102  f1otrg  29201  ax5seg  29269  axcontlem4  29298  eengtrkg  29317  wlkonwlk1l  29992  crctcshwlkn0  30151  wwlksnextinj  30229  wwlksnextsurj  30230  clwwlkf1  30381  clwwlknon1  30429  numclwwlk1lem2f1  30689  wlkl0  30699  grpoidinv  30841  pjnmopi  32481  cdj1i  32766  xrofsup  33093  ccfldsrarelvec  34042  dya2iocnrect  34652  omssubadd  34671  sitgfval  34712  bnj969  35315  bnj1463  35424  erdszelem7  35670  rellysconn  35724  segconeq  36483  ifscgr  36517  btwnconn1lem13  36572  btwnconn1lem14  36573  outsideofeq  36603  ellines  36625  fnessref  36849  refssfne  36850  knoppndvlem14  37095  isbasisrelowllem1  37982  isbasisrelowllem2  37983  relowlssretop  37990  itg2gt0cn  38307  frinfm  38367  heiborlem3  38445  isfldidl  38700  eldisjs6  39570  4atlem12  40367  cdleme48fv  41254  cdlemg35  41468  mapd0  42420  aks4d1p1p5  42823  flt4lem7  43374  nna4b4nsq  43375  3cubeslem1  43398  mzpincl  43448  mzpindd  43460  diophin  43486  pellexlem3  43541  pellexlem5  43543  dfno2  44137  amgm3d  44908  amgm4d  44909  lptre2pt  46337  dvnprodlem2  46644  stoweidlem1  46698  stoweidlem14  46711  stoweidlem17  46714  stoweidlem27  46724  stoweidlem57  46754  fourierdlem12  46816  fourierdlem14  46818  fourierdlem70  46873  fourierdlem92  46895  fourierdlem111  46914  etransclem10  46941  etransclem24  46955  salgenval  47018  smfaddlem1  47460  f1cof1blem  47794  elfzelfzlble  48041  reuopreuprim  48258  gpgedgvtx0  48809  rngcinvALTV  49024  ringcinvALTV  49058  lmod1  49255  inlinecirc02plem  49549  nelsubclem  49828  oppf1st2nd  49892