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  6167  xpdifcnvepel  6168  tpres  7203  f1oiso2  7356  poseq  8156  oewordri  8580  boxriin  8940  cantnfrescl  9648  cfsuc  10252  prsrlem1  11068  lemulge11  12088  lediv12a  12119  elnnz  12612  quoremz  13902  quoremnn0ALT  13904  fldiv  13907  modsumfzodifsn  13994  leexp1a  14225  faclbnd6  14349  wrdlen2i  14999  wwlktovfo  15015  setcinv  18165  sgrp2rid2  19012  grpidinv2  19088  eqg0subg  19291  gsumval3lem1  19999  rhmopp  20636  rngcinv  20766  ringcinv  20800  dvdsrzring  21641  cncnp2  23468  vitalilem1  25798  aaliou3lem2  26537  2sqreulem1  27641  2sqreunnlem1  27644  pntibndlem2  27786  elnnzs  28625  tgjustf  28773  iscgrglt  28814  islnoppd  29052  oppcom  29056  opphllem1  29059  opphllem5  29063  oppperpex  29065  hpgerlem  29078  colhp  29083  prlngsym  29222  ax5seg  29319  uhgr2edg  29592  nbupgrres  29748  usgr2pthlem  30152  crctcshwlkn0lem5  30206  clwwlknonwwlknonb  30500  1pthond  30538  3pthdlem1  30562  frgrwopreglem5a  30709  grpoidinv  30907  nmcvcn  31094  leopmul  32533  resf1o  33121  trsp2cyc  33483  oddpwdc  34785  btwnconn1  36606  finminlem  36862  ptrecube  38304  poimirlem22  38326  isrngod  38582  paddasslem4  40630  cdleme21h  41141  cdleme26eALTN  41168  cdleme40m  41274  cdlemf2  41369  dicssdvh  41993  dihopelvalcpre  42055  dihmeetlem4preN  42113  dih1dimatlem0  42135  primrootscoprmpow  42899  primrootscoprbij  42902  aks6d1c5  42939  sticksstones22  42968  aks6d1c6lem3  42972  unitscyglem3  42997  unitscyglem5  42999  lzenom  43534  jm2.27c  43767  omltoe  44166  clrellem  44381  2pm13.193  45294  disjxp1  45822  dmrelrnrel  45975  infleinflem2  46119  mullimc  46365  mullimcf  46372  addlimc  46395  0ellimcdiv  46396  icccncfext  46634  stoweidlem52  46799  wallispilem4  46815  fourierdlem16  46870  fourierdlem21  46875  fourierdlem48  46901  fourierdlem51  46904  fourierdlem52  46905  fourierdlem54  46907  fourierdlem64  46917  fourierdlem76  46929  fourierdlem77  46930  fourierdlem80  46933  fourierdlem86  46939  fourierdlem87  46940  fourierdlem102  46955  fourierdlem114  46967  sge0f1o  47129  sge0split  47156  nnfoctbdjlem  47202  iundjiun  47207  ismeannd  47214  psmeasure  47218  isomennd  47278  hoidmvle  47347  ovncvr2  47358  dfatbrafv2b  48015  oexpnegnz  48476  clnbgrgrim  48732  usgrexmpl2trifr  48835  rngcinvALTV  49074  ringcinvALTV  49108  itsclc0b  49585  seposep  49737