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  3842  domssl  8920  domssr  8921  sbthlem9  9008  nqerf  10821  lemul12a  11979  lediv12a  12015  elfzd  13415  fzass4  13462  4fvwrd4  13548  leexp1a  14082  wrd2ind  14630  cshwidxm1  14714  rtrclreclem4  14968  coprmproddvdslem  16573  reumodprminv  16716  prmgaplem6  16968  mreexexlem2d  17551  sgrp2nmndlem4  18836  pmtrrn2  19372  rngcinv  20552  ringcinv  20586  islmodd  20799  nn0srg  21374  rge0srg  21375  mdet1  22516  cpmatmcllem  22633  neitr  23095  restnlly  23397  llyrest  23400  llyidm  23403  uptx  23540  alexsubALTlem2  23963  alexsubALTlem4  23965  distspace  24231  ncvs1  25084  ivthlem3  25381  conway  27740  uzsind  28329  renegscl  28400  readdscl  28401  remulscl  28404  axtg5seg  28443  colperpexlem3  28710  outpasch  28733  iscgra1  28788  f1otrg  28849  ax5seg  28916  axcontlem4  28945  eengtrkg  28964  wlkonwlk1l  29640  crctcshwlkn0  29799  wwlksnextinj  29877  wwlksnextsurj  29878  clwwlkf1  30029  clwwlknon1  30077  numclwwlk1lem2f1  30337  wlkl0  30347  grpoidinv  30488  pjnmopi  32128  cdj1i  32413  xrofsup  32750  ccfldsrarelvec  33684  dya2iocnrect  34294  omssubadd  34313  sitgfval  34354  bnj969  34958  bnj1463  35067  erdszelem7  35241  rellysconn  35295  segconeq  36054  ifscgr  36088  btwnconn1lem13  36143  btwnconn1lem14  36144  outsideofeq  36174  ellines  36196  fnessref  36401  refssfne  36402  knoppndvlem14  36569  isbasisrelowllem1  37399  isbasisrelowllem2  37400  relowlssretop  37407  itg2gt0cn  37714  frinfm  37774  heiborlem3  37852  isfldidl  38107  4atlem12  39710  cdleme48fv  40597  cdlemg35  40811  mapd0  41763  aks4d1p1p5  42167  flt4lem7  42751  nna4b4nsq  42752  3cubeslem1  42776  mzpincl  42826  mzpindd  42838  diophin  42864  pellexlem3  42923  pellexlem5  42925  dfno2  43520  amgm3d  44291  amgm4d  44292  lptre2pt  45737  dvnprodlem2  46044  stoweidlem1  46098  stoweidlem14  46111  stoweidlem17  46114  stoweidlem27  46124  stoweidlem57  46154  fourierdlem12  46216  fourierdlem14  46218  fourierdlem70  46273  fourierdlem92  46295  fourierdlem111  46314  etransclem10  46341  etransclem24  46355  salgenval  46418  smfaddlem1  46860  f1cof1blem  47173  elfzelfzlble  47420  reuopreuprim  47625  gpgedgvtx0  48160  rngcinvALTV  48375  ringcinvALTV  48409  lmod1  48592  inlinecirc02plem  48886  nelsubclem  49167  oppf1st2nd  49231