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  6121  tpres  7141  f1oiso2  7293  poseq  8098  oewordri  8517  boxriin  8874  cantnfrescl  9591  cfsuc  10170  prsrlem1  10985  lemulge11  12006  lediv12a  12037  elnnz  12500  quoremz  13778  quoremnn0ALT  13780  fldiv  13783  modsumfzodifsn  13870  leexp1a  14101  faclbnd6  14225  wrdlen2i  14868  wwlktovfo  14884  setcinv  18016  sgrp2rid2  18819  grpidinv2  18895  eqg0subg  19094  gsumval3lem1  19803  rhmopp  20413  rngcinv  20541  ringcinv  20575  dvdsrzring  21387  cncnp2  23185  vitalilem1  25526  aaliou3lem2  26268  2sqreulem1  27374  2sqreunnlem1  27377  pntibndlem2  27519  elnnzs  28313  tgjustf  28437  iscgrglt  28478  islnoppd  28704  oppcom  28708  opphllem1  28711  opphllem5  28715  oppperpex  28717  hpgerlem  28729  colhp  28734  ax5seg  28902  uhgr2edg  29172  nbupgrres  29328  usgr2pthlem  29727  crctcshwlkn0lem5  29778  clwwlknonwwlknonb  30069  1pthond  30107  3pthdlem1  30127  frgrwopreglem5a  30274  grpoidinv  30471  nmcvcn  30658  leopmul  32097  resf1o  32692  trsp2cyc  33084  oddpwdc  34341  btwnconn1  36094  finminlem  36311  ptrecube  37619  poimirlem22  37641  isrngod  37897  paddasslem4  39822  cdleme21h  40333  cdleme26eALTN  40360  cdleme40m  40466  cdlemf2  40561  dicssdvh  41185  dihopelvalcpre  41247  dihmeetlem4preN  41305  dih1dimatlem0  41327  primrootscoprmpow  42092  primrootscoprbij  42095  aks6d1c5  42132  sticksstones22  42161  aks6d1c6lem3  42165  unitscyglem3  42190  unitscyglem5  42192  lzenom  42763  jm2.27c  43000  omltoe  43400  clrellem  43615  2pm13.193  44546  disjxp1  45067  dmrelrnrel  45224  infleinflem2  45370  mullimc  45617  mullimcf  45624  addlimc  45649  0ellimcdiv  45650  icccncfext  45888  stoweidlem52  46053  wallispilem4  46069  fourierdlem16  46124  fourierdlem21  46129  fourierdlem48  46155  fourierdlem51  46158  fourierdlem52  46159  fourierdlem54  46161  fourierdlem64  46171  fourierdlem76  46183  fourierdlem77  46184  fourierdlem80  46187  fourierdlem86  46193  fourierdlem87  46194  fourierdlem102  46209  fourierdlem114  46221  sge0f1o  46383  sge0split  46410  nnfoctbdjlem  46456  iundjiun  46461  ismeannd  46468  psmeasure  46472  isomennd  46532  hoidmvle  46601  ovncvr2  46612  dfatbrafv2b  47249  oexpnegnz  47682  clnbgrgrim  47938  usgrexmpl2trifr  48041  rngcinvALTV  48280  ringcinvALTV  48314  itsclc0b  48777  seposep  48930