Theorem jca32 556

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  syl12anc  1316  sbthlem9  7963  nqerf  9631  lemul12a  10760  lediv12a  10795  fzass4  12250  elfz1b  12279  4fvwrd4  12328  leexp1a  12781  wrd2ind  13329  cshwidxm1  13404  rtrclreclem4  13649  coprmproddvdslem  15214  prmgaplem6  15598  mreexexlem2d  16128  sgrp2nmndlem4  17238  pmtrrn2  17703  islmodd  18692  nn0srg  19635  rge0srg  19636  mdet1  20226  cpmatmcllem  20342  neitr  20794  restnlly  21095  llyrest  21098  llyidm  21101  uptx  21238  alexsubALTlem2  21662  alexsubALTlem4  21664  distspace  21931  ncvs1  22765  ivthlem3  23029  axtg5seg  25164  colperpexlem3  25424  outpasch  25447  iscgra1  25502  f1otrg  25551  ax5seg  25618  axcontlem4  25647  eengtrkg  25665  wwlkextinj  26258  wwlkextsur  26259  clwwlkf1  26324  usg2spot2nb  26592  grpoidinv  26746  pjnmopi  28391  cdj1i  28676  xrofsup  28923  dya2iocnrect  29670  omssubadd  29689  sitgfval  29730  bnj969  30270  bnj1463  30377  erdszelem7  30433  rellyscon  30487  segconeq  31287  ifscgr  31321  btwnconn1lem13  31376  btwnconn1lem14  31377  outsideofeq  31407  ellines  31429  fnessref  31522  refssfne  31523  knoppndvlem14  31686  isbasisrelowllem1  32379  isbasisrelowllem2  32380  relowlssretop  32387  itg2gt0cn  32635  frinfm  32700  heiborlem3  32782  isfldidl  33037  4atlem12  33916  cdleme48fv  34805  cdlemg35  35019  mapd0  35972  mzpincl  36315  mzpindd  36327  diophin  36354  pellexlem3  36413  pellexlem5  36415  amgm3d  37524  amgm4d  37525  monoords  38452  uzfissfz  38483  iuneqfzuzlem  38491  ssuzfz  38506  mccllem  38664  sumnnodd  38697  lptre2pt  38707  dvnmul  38833  dvnprodlem1  38836  dvnprodlem2  38837  itgspltprt  38871  stoweidlem1  38894  stoweidlem3  38896  stoweidlem14  38907  stoweidlem17  38910  stoweidlem27  38920  stoweidlem57  38950  fourierdlem12  39012  fourierdlem14  39014  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem70  39069  fourierdlem79  39078  fourierdlem92  39091  fourierdlem111  39110  elaa2lem  39126  etransclem3  39130  etransclem7  39134  etransclem10  39137  etransclem24  39151  etransclem27  39154  etransclem28  39155  etransclem35  39162  etransclem38  39165  etransclem44  39171  salgenval  39217  iundjiun  39353  caratheodorylem1  39416  smfaddlem1  39649  reuan  39829  elfzelfzlble  40358  wlkOnwlk1l  40871  crctcsh1wlkn0  41024  wwlksnextinj  41105  wwlksnextsur  41106  clwwlksf1  41224  fusgr2wsp2nb  41498  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  lmod1  42075