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  3843  domssl  9029  domssr  9030  sbthlem9  9118  nqerf  11019  lemul12a  12179  lediv12a  12214  elfzd  13651  fzass4  13700  4fvwrd4  13786  leexp1a  14322  wrd2ind  14877  cshwidxm1  14963  rtrclreclem4  15220  coprmproddvdslem  16843  reumodprminv  16988  prmgaplem6  17240  mreexexlem2d  17825  sgrp2nmndlem4  19133  pmtrrn2  19680  rngcinv  20895  ringcinv  20929  islmodd  21147  nn0srg  21749  rge0srg  21750  mdet1  22922  cpmatmcllem  23042  neitr  23504  restnlly  23807  llyrest  23810  llyidm  23813  uptx  23950  alexsubALTlem2  24373  alexsubALTlem4  24375  distspace  24641  ncvs1  25484  ivthlem3  25780  flt4lem7  27995  nna4b4nsq  27996  conway  28171  uzsind  28797  renegscl  28890  readdscl  28891  remulscl  28894  axtg5seg  28933  tglnpt3  29128  colperpexlem3  29214  outpasch  29239  iscgra1  29323  f1otrg  29454  ax5seg  29522  axcontlem4  29551  eengtrkg  29570  wlkonwlk1l  30248  crctcshwlkn0  30416  wwlksnextinj  30494  wwlksnextsurj  30495  clwwlkf1  30646  clwwlknon1  30694  numclwwlk1lem2f1  30964  wlkl0  30974  grpoidinv  31116  pjnmopi  32756  cdj1i  33041  xrofsup  33406  ccfldsrarelvec  34350  dya2iocnrect  34960  omssubadd  34979  sitgfval  35020  bnj969  35623  bnj1463  35732  erdszelem7  36049  rellysconn  36103  segconeq  36868  ifscgr  36902  btwnconn1lem13  36957  btwnconn1lem14  36958  outsideofeq  36988  ellines  37010  fnessref  37238  refssfne  37239  knoppndvlem14  37484  isbasisrelowllem1  38372  isbasisrelowllem2  38373  relowlssretop  38380  itg2gt0cn  38687  frinfm  38763  heiborlem3  38841  isfldidl  39096  eldisjs6  39966  4atlem12  40763  cdleme48fv  41650  cdlemg35  41864  mapd0  42816  aks4d1p1p5  43219  3cubeslem1  43788  mzpincl  43839  mzpindd  43851  diophin  43877  pellexlem3  43932  pellexlem5  43934  dfno2  44523  amgm3d  45293  amgm4d  45294  lptre2pt  46744  dvnprodlem2  47051  stoweidlem1  47105  stoweidlem14  47118  stoweidlem17  47121  stoweidlem27  47131  stoweidlem57  47161  fourierdlem12  47223  fourierdlem14  47225  fourierdlem70  47280  fourierdlem92  47302  fourierdlem111  47321  etransclem10  47348  etransclem24  47362  salgenval  47425  smfaddlem1  47867  f1cof1blem  48238  elfzelfzlble  48485  reuopreuprim  48702  gpgedgvtx0  49253  rngcinvALTV  49467  ringcinvALTV  49501  lmod1  49698  inlinecirc02plem  49992  nelsubclem  50275  oppf1st2nd  50341  parmapcl2  50864