Theorem jca31 524

Description: Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.)

Hypotheses

Ref	Expression
jca31.1	⊢ (𝜑 → 𝜓)
jca31.2	⊢ (𝜑 → 𝜒)
jca31.3	⊢ (𝜑 → 𝜃)

Assertion

Ref	Expression
jca31	⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))

Proof of Theorem jca31

Step	Hyp	Ref	Expression
1		jca31.1	. . 3 ⊢ (𝜑 → 𝜓)
2		jca31.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 521	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		jca31.3	. 2 ⊢ (𝜑 → 𝜃)
5	3, 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:  3jca  1146  syl21anbrc  1363  xpdifid  6158  xpdifcnvepel  6159  tpres  7208  f1oiso2  7361  poseq  8178  oewordri  8605  boxriin  8972  cantnfrescl  9681  cfsuc  10339  prsrlem1  11161  lemulge11  12183  lediv12a  12214  elnnz  12707  quoremz  13999  quoremnn0ALT  14001  fldiv  14004  modsumfzodifsn  14091  leexp1a  14322  faclbnd6  14447  wrdlen2i  15099  wwlktovfo  15117  setcinv  18271  sgrp2rid2  19131  grpidinv2  19214  eqg0subg  19417  gsumval3lem1  20125  rhmopp  20765  rngcinv  20895  ringcinv  20929  dvdsrzring  21773  cncnp2  23605  vitalilem1  25935  aaliou3lem2  26676  2sqreulem1  27779  2sqreunnlem1  27782  pntibndlem2  27924  elnnzs  28793  tgjustf  28941  iscgrglt  28983  islnoppd  29222  oppcom  29226  opphllem1  29229  opphllem5  29233  oppperpex  29235  hpgerlem  29249  colhp  29254  prlngsym  29425  ax5seg  29522  uhgr2edg  29795  nbupgrres  29951  usgr2pthlem  30355  crctcshwlkn0lem5  30409  clwwlknonwwlknonb  30703  1pthond  30741  3pthdlem1  30771  frgrwopreglem5a  30918  grpoidinv  31116  nmcvcn  31303  leopmul  32742  resf1o  33369  trsp2cyc  33731  oddpwdc  35033  btwnconn1  36959  finminlem  37199  ptrecube  38632  poimirlem22  38654  isrngod  38926  paddasslem4  40974  cdleme21h  41485  cdleme26eALTN  41512  cdleme40m  41618  cdlemf2  41713  dicssdvh  42337  dihopelvalcpre  42399  dihmeetlem4preN  42457  dih1dimatlem0  42479  primrootscoprmpow  43243  primrootscoprbij  43246  aks6d1c5  43283  sticksstones22  43312  aks6d1c6lem3  43316  unitscyglem3  43341  unitscyglem5  43343  lzenom  43875  jm2.27c  44108  omltoe  44502  clrellem  44716  2pm13.193  45629  disjxp1  46180  dmrelrnrel  46333  infleinflem2  46476  mullimc  46722  mullimcf  46729  addlimc  46752  0ellimcdiv  46753  icccncfext  46991  stoweidlem52  47156  wallispilem4  47172  fourierdlem16  47227  fourierdlem21  47232  fourierdlem48  47258  fourierdlem51  47261  fourierdlem52  47262  fourierdlem54  47264  fourierdlem64  47274  fourierdlem76  47286  fourierdlem77  47287  fourierdlem80  47290  fourierdlem86  47296  fourierdlem87  47297  fourierdlem102  47312  fourierdlem114  47324  sge0f1o  47486  sge0split  47513  nnfoctbdjlem  47559  iundjiun  47564  ismeannd  47571  psmeasure  47575  isomennd  47635  hoidmvle  47704  ovncvr2  47715  dfatbrafv2b  48409  oexpnegnz  48870  clnbgrgrim  49126  usgrexmpl2trifr  49229  rngcinvALTV  49467  ringcinvALTV  49501  itsclc0b  49978  seposep  50134