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  6177  xpdifcnvepel  6178  tpres  7238  f1oiso2  7391  poseq  8212  oewordri  8639  boxriin  9006  cantnfrescl  9714  cfsuc  10374  prsrlem1  11196  lemulge11  12219  lediv12a  12250  elnnz  12743  quoremz  14035  quoremnn0ALT  14037  fldiv  14040  modsumfzodifsn  14127  leexp1a  14358  faclbnd6  14484  wrdlen2i  15136  wwlktovfo  15154  setcinv  18315  sgrp2rid2  19175  grpidinv2  19258  eqg0subg  19461  gsumval3lem1  20170  rhmopp  20810  rngcinv  20940  ringcinv  20974  dvdsrzring  21822  cncnp2  23654  vitalilem1  25984  aaliou3lem2  26727  2sqreulem1  27830  2sqreunnlem1  27833  pntibndlem2  27975  elnnzs  28844  tgjustf  28992  iscgrglt  29034  islnoppd  29273  oppcom  29277  opphllem1  29280  opphllem5  29284  oppperpex  29286  hpgerlem  29300  colhp  29305  prlngsym  29476  ax5seg  29573  uhgr2edg  29846  nbupgrres  30002  usgr2pthlem  30406  crctcshwlkn0lem5  30460  clwwlknonwwlknonb  30754  1pthond  30792  3pthdlem1  30822  frgrwopreglem5a  30969  grpoidinv  31167  nmcvcn  31354  leopmul  32793  resf1o  33418  trsp2cyc  33783  oddpwdc  35097  btwnconn1  37081  finminlem  37321  ptrecube  38806  poimirlem22  38828  isrngod  39098  paddasslem4  41146  cdleme21h  41657  cdleme26eALTN  41684  cdleme40m  41790  cdlemf2  41885  dicssdvh  42509  dihopelvalcpre  42571  dihmeetlem4preN  42629  dih1dimatlem0  42651  primrootscoprmpow  43415  primrootscoprbij  43418  aks6d1c5  43455  sticksstones22  43484  aks6d1c6lem3  43488  unitscyglem3  43513  unitscyglem5  43515  lzenom  44047  jm2.27c  44280  omltoe  44669  clrellem  44883  2pm13.193  45795  disjxp1  46360  dmrelrnrel  46512  infleinflem2  46655  mullimc  46901  mullimcf  46908  addlimc  46931  0ellimcdiv  46932  icccncfext  47170  stoweidlem52  47335  wallispilem4  47351  fourierdlem16  47406  fourierdlem21  47411  fourierdlem48  47437  fourierdlem51  47440  fourierdlem52  47441  fourierdlem54  47443  fourierdlem64  47453  fourierdlem76  47465  fourierdlem77  47466  fourierdlem80  47469  fourierdlem86  47475  fourierdlem87  47476  fourierdlem102  47491  fourierdlem114  47503  sge0f1o  47665  sge0split  47692  nnfoctbdjlem  47738  iundjiun  47743  ismeannd  47750  psmeasure  47754  isomennd  47814  hoidmvle  47883  ovncvr2  47894  dfatbrafv2b  48588  oexpnegnz  49049  clnbgrgrim  49305  usgrexmpl2trifr  49408  rngcinvALTV  49646  ringcinvALTV  49680  itsclc0b  50215  seposep  50371