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  3853  domssl  9004  domssr  9005  sbthlem9  9093  nqerf  10933  lemul12a  12091  lediv12a  12126  elfzd  13561  fzass4  13609  4fvwrd4  13695  leexp1a  14231  wrd2ind  14784  cshwidxm1  14870  rtrclreclem4  15124  coprmproddvdslem  16745  reumodprminv  16889  prmgaplem6  17141  mreexexlem2d  17726  sgrp2nmndlem4  19021  pmtrrn2  19561  rngcinv  20773  ringcinv  20807  islmodd  21024  nn0srg  21624  rge0srg  21625  mdet1  22795  cpmatmcllem  22912  neitr  23374  restnlly  23676  llyrest  23679  llyidm  23682  uptx  23819  alexsubALTlem2  24242  alexsubALTlem4  24244  distspace  24510  ncvs1  25353  ivthlem3  25649  conway  28009  uzsind  28635  renegscl  28728  readdscl  28729  remulscl  28732  axtg5seg  28771  tglnpt3  28964  colperpexlem3  29050  outpasch  29074  iscgra1  29158  f1otrg  29257  ax5seg  29325  axcontlem4  29354  eengtrkg  29373  wlkonwlk1l  30048  crctcshwlkn0  30207  wwlksnextinj  30285  wwlksnextsurj  30286  clwwlkf1  30437  clwwlknon1  30485  numclwwlk1lem2f1  30745  wlkl0  30755  grpoidinv  30897  pjnmopi  32537  cdj1i  32822  xrofsup  33149  ccfldsrarelvec  34092  dya2iocnrect  34703  omssubadd  34722  sitgfval  34763  bnj969  35366  bnj1463  35475  erdszelem7  35710  rellysconn  35764  segconeq  36523  ifscgr  36557  btwnconn1lem13  36612  btwnconn1lem14  36613  outsideofeq  36643  ellines  36665  fnessref  36909  refssfne  36910  knoppndvlem14  37155  isbasisrelowllem1  38042  isbasisrelowllem2  38043  relowlssretop  38050  itg2gt0cn  38367  frinfm  38427  heiborlem3  38505  isfldidl  38760  eldisjs6  39630  4atlem12  40427  cdleme48fv  41314  cdlemg35  41528  mapd0  42480  aks4d1p1p5  42883  flt4lem7  43432  nna4b4nsq  43433  3cubeslem1  43456  mzpincl  43506  mzpindd  43518  diophin  43544  pellexlem3  43599  pellexlem5  43601  dfno2  44195  amgm3d  44966  amgm4d  44967  lptre2pt  46395  dvnprodlem2  46702  stoweidlem1  46756  stoweidlem14  46769  stoweidlem17  46772  stoweidlem27  46782  stoweidlem57  46812  fourierdlem12  46874  fourierdlem14  46876  fourierdlem70  46931  fourierdlem92  46953  fourierdlem111  46972  etransclem10  46999  etransclem24  47013  salgenval  47076  smfaddlem1  47518  f1cof1blem  47852  elfzelfzlble  48099  reuopreuprim  48316  gpgedgvtx0  48867  rngcinvALTV  49082  ringcinvALTV  49116  lmod1  49313  inlinecirc02plem  49607  nelsubclem  49886  oppf1st2nd  49950