Theorem jca32 525

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  reuan  3848  frinf  6311  domssl  9056  domssr  9057  sbthlem9  9145  nqerf  11045  lemul12a  12205  lediv12a  12240  elfzd  13677  fzass4  13726  4fvwrd4  13812  leexp1a  14348  wrd2ind  14903  cshwidxm1  14989  rtrclreclem4  15246  coprmproddvdslem  16869  reumodprminv  17014  prmgaplem6  17266  mreexexlem2d  17851  sgrp2nmndlem4  19159  pmtrrn2  19707  rngcinv  20922  ringcinv  20956  islmodd  21174  nn0srg  21776  rge0srg  21777  mdet1  22949  cpmatmcllem  23069  neitr  23531  restnlly  23834  llyrest  23837  llyidm  23840  uptx  23977  alexsubALTlem2  24400  alexsubALTlem4  24402  distspace  24668  ncvs1  25511  ivthlem3  25807  flt4lem7  28022  nna4b4nsq  28023  conway  28198  uzsind  28824  renegscl  28917  readdscl  28918  remulscl  28921  axtg5seg  28960  tglnpt3  29155  colperpexlem3  29241  outpasch  29266  iscgra1  29350  f1otrg  29481  ax5seg  29549  axcontlem4  29578  eengtrkg  29597  wlkonwlk1l  30275  crctcshwlkn0  30443  wwlksnextinj  30521  wwlksnextsurj  30522  clwwlkf1  30673  clwwlknon1  30721  numclwwlk1lem2f1  30991  wlkl0  31001  grpoidinv  31143  pjnmopi  32783  cdj1i  33068  xrofsup  33432  ccfldsrarelvec  34386  dya2iocnrect  34996  omssubadd  35015  sitgfval  35056  bnj969  35659  bnj1463  35768  erdszelem7  36142  rellysconn  36196  segconeq  36966  ifscgr  37000  btwnconn1lem13  37055  btwnconn1lem14  37056  outsideofeq  37086  ellines  37108  fnessref  37336  refssfne  37337  knoppndvlem14  37582  isbasisrelowllem1  38483  isbasisrelowllem2  38484  relowlssretop  38491  itg2gt0cn  38798  heiborlem3  38950  isfldidl  39205  eldisjs6  40075  4atlem12  40872  cdleme48fv  41759  cdlemg35  41973  mapd0  42925  aks4d1p1p5  43328  3cubeslem1  43898  mzpincl  43949  mzpindd  43961  diophin  43987  pellexlem3  44042  pellexlem5  44044  dfno2  44632  amgm3d  45402  amgm4d  45403  lptre2pt  46865  dvnprodlem2  47172  stoweidlem1  47226  stoweidlem14  47239  stoweidlem17  47242  stoweidlem27  47252  stoweidlem57  47282  fourierdlem12  47344  fourierdlem14  47346  fourierdlem70  47401  fourierdlem92  47423  fourierdlem111  47442  etransclem10  47469  etransclem24  47483  salgenval  47546  smfaddlem1  47988  f1cof1blem  48359  elfzelfzlble  48606  reuopreuprim  48823  gpgedgvtx0  49374  rngcinvALTV  49588  ringcinvALTV  49622  lmod1  49819  inlinecirc02plem  50113  nelsubclem  50396  oppf1st2nd  50462  parmapcl2  50985