Theorem jca32 516

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 512	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5	1, 4	jca 512	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 206  df-an 397

This theorem is referenced by:  reuan  3840  domssl  8859  domssr  8860  sbthlem9  8956  nqerf  10787  lemul12a  11934  lediv12a  11969  elfzd  13348  fzass4  13395  4fvwrd4  13477  leexp1a  13994  wrd2ind  14534  cshwidxm1  14618  rtrclreclem4  14871  coprmproddvdslem  16464  reumodprminv  16602  prmgaplem6  16854  mreexexlem2d  17451  sgrp2nmndlem4  18663  pmtrrn2  19164  islmodd  20235  nn0srg  20774  rge0srg  20775  mdet1  21856  cpmatmcllem  21973  neitr  22437  restnlly  22739  llyrest  22742  llyidm  22745  uptx  22882  alexsubALTlem2  23305  alexsubALTlem4  23307  distspace  23575  ncvs1  24427  ivthlem3  24723  conway  27044  axtg5seg  27115  colperpexlem3  27382  outpasch  27405  iscgra1  27460  f1otrg  27521  ax5seg  27595  axcontlem4  27624  eengtrkg  27643  wlkonwlk1l  28319  crctcshwlkn0  28474  wwlksnextinj  28552  wwlksnextsurj  28553  clwwlkf1  28701  clwwlknon1  28749  numclwwlk1lem2f1  29009  wlkl0  29019  grpoidinv  29158  pjnmopi  30798  cdj1i  31083  xrofsup  31377  ccfldsrarelvec  32039  dya2iocnrect  32548  omssubadd  32567  sitgfval  32608  bnj969  33225  bnj1463  33334  erdszelem7  33458  rellysconn  33512  segconeq  34408  ifscgr  34442  btwnconn1lem13  34497  btwnconn1lem14  34498  outsideofeq  34528  ellines  34550  fnessref  34642  refssfne  34643  knoppndvlem14  34801  isbasisrelowllem1  35631  isbasisrelowllem2  35632  relowlssretop  35639  itg2gt0cn  35937  frinfm  35998  heiborlem3  36076  isfldidl  36331  4atlem12  37880  cdleme48fv  38767  cdlemg35  38981  mapd0  39933  leexp1ad  40234  aks4d1p1p5  40337  flt4lem7  40758  nna4b4nsq  40759  3cubeslem1  40768  mzpincl  40818  mzpindd  40830  diophin  40856  pellexlem3  40915  pellexlem5  40917  dfno2  41357  amgm3d  42131  amgm4d  42132  lptre2pt  43517  dvnprodlem2  43824  stoweidlem1  43878  stoweidlem14  43891  stoweidlem17  43894  stoweidlem27  43904  stoweidlem57  43934  fourierdlem12  43996  fourierdlem14  43998  fourierdlem70  44053  fourierdlem92  44075  fourierdlem111  44094  etransclem10  44121  etransclem24  44135  salgenval  44198  smfaddlem1  44638  f1cof1blem  44919  elfzelfzlble  45164  reuopreuprim  45329  rngcinv  45890  rngcinvALTV  45902  ringcinv  45941  ringcinvALTV  45965  lmod1  46184  inlinecirc02plem  46483