Theorem jca31 514

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  3jca  1128  syl21anbrc  1345  xpdifid  6141  tpres  7175  f1oiso2  7327  poseq  8137  oewordri  8556  boxriin  8913  cantnfrescl  9629  cfsuc  10210  prsrlem1  11025  lemulge11  12045  lediv12a  12076  elnnz  12539  quoremz  13817  quoremnn0ALT  13819  fldiv  13822  modsumfzodifsn  13909  leexp1a  14140  faclbnd6  14264  wrdlen2i  14908  wwlktovfo  14924  setcinv  18052  sgrp2rid2  18853  grpidinv2  18929  eqg0subg  19128  gsumval3lem1  19835  rhmopp  20418  rngcinv  20546  ringcinv  20580  dvdsrzring  21371  cncnp2  23168  vitalilem1  25509  aaliou3lem2  26251  2sqreulem1  27357  2sqreunnlem1  27360  pntibndlem2  27502  elnnzs  28289  tgjustf  28400  iscgrglt  28441  islnoppd  28667  oppcom  28671  opphllem1  28674  opphllem5  28678  oppperpex  28680  hpgerlem  28692  colhp  28697  ax5seg  28865  uhgr2edg  29135  nbupgrres  29291  usgr2pthlem  29693  crctcshwlkn0lem5  29744  clwwlknonwwlknonb  30035  1pthond  30073  3pthdlem1  30093  frgrwopreglem5a  30240  grpoidinv  30437  nmcvcn  30624  leopmul  32063  resf1o  32653  trsp2cyc  33080  oddpwdc  34345  btwnconn1  36089  finminlem  36306  ptrecube  37614  poimirlem22  37636  isrngod  37892  paddasslem4  39817  cdleme21h  40328  cdleme26eALTN  40355  cdleme40m  40461  cdlemf2  40556  dicssdvh  41180  dihopelvalcpre  41242  dihmeetlem4preN  41300  dih1dimatlem0  41322  primrootscoprmpow  42087  primrootscoprbij  42090  aks6d1c5  42127  sticksstones22  42156  aks6d1c6lem3  42160  unitscyglem3  42185  unitscyglem5  42187  lzenom  42758  jm2.27c  42996  omltoe  43396  clrellem  43611  2pm13.193  44542  disjxp1  45063  dmrelrnrel  45220  infleinflem2  45367  mullimc  45614  mullimcf  45621  addlimc  45646  0ellimcdiv  45647  icccncfext  45885  stoweidlem52  46050  wallispilem4  46066  fourierdlem16  46121  fourierdlem21  46126  fourierdlem48  46152  fourierdlem51  46155  fourierdlem52  46156  fourierdlem54  46158  fourierdlem64  46168  fourierdlem76  46180  fourierdlem77  46181  fourierdlem80  46184  fourierdlem86  46190  fourierdlem87  46191  fourierdlem102  46206  fourierdlem114  46218  sge0f1o  46380  sge0split  46407  nnfoctbdjlem  46453  iundjiun  46458  ismeannd  46465  psmeasure  46469  isomennd  46529  hoidmvle  46598  ovncvr2  46609  dfatbrafv2b  47246  oexpnegnz  47679  clnbgrgrim  47934  usgrexmpl2trifr  48028  rngcinvALTV  48264  ringcinvALTV  48298  itsclc0b  48761  seposep  48914