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  1129  syl21anbrc  1346  xpdifid  6134  tpres  7157  f1oiso2  7308  poseq  8110  oewordri  8530  boxriin  8890  cantnfrescl  9597  cfsuc  10179  prsrlem1  10995  lemulge11  12016  lediv12a  12047  elnnz  12510  quoremz  13787  quoremnn0ALT  13789  fldiv  13792  modsumfzodifsn  13879  leexp1a  14110  faclbnd6  14234  wrdlen2i  14877  wwlktovfo  14893  setcinv  18026  sgrp2rid2  18863  grpidinv2  18939  eqg0subg  19137  gsumval3lem1  19846  rhmopp  20454  rngcinv  20582  ringcinv  20616  dvdsrzring  21428  cncnp2  23237  vitalilem1  25577  aaliou3lem2  26319  2sqreulem1  27425  2sqreunnlem1  27428  pntibndlem2  27570  elnnzs  28409  tgjustf  28557  iscgrglt  28598  islnoppd  28824  oppcom  28828  opphllem1  28831  opphllem5  28835  oppperpex  28837  hpgerlem  28849  colhp  28854  ax5seg  29023  uhgr2edg  29293  nbupgrres  29449  usgr2pthlem  29848  crctcshwlkn0lem5  29899  clwwlknonwwlknonb  30193  1pthond  30231  3pthdlem1  30251  frgrwopreglem5a  30398  grpoidinv  30596  nmcvcn  30783  leopmul  32222  resf1o  32820  trsp2cyc  33217  oddpwdc  34532  btwnconn1  36317  finminlem  36534  ptrecube  37871  poimirlem22  37893  isrngod  38149  paddasslem4  40199  cdleme21h  40710  cdleme26eALTN  40737  cdleme40m  40843  cdlemf2  40938  dicssdvh  41562  dihopelvalcpre  41624  dihmeetlem4preN  41682  dih1dimatlem0  41704  primrootscoprmpow  42469  primrootscoprbij  42472  aks6d1c5  42509  sticksstones22  42538  aks6d1c6lem3  42542  unitscyglem3  42567  unitscyglem5  42569  lzenom  43127  jm2.27c  43364  omltoe  43763  clrellem  43978  2pm13.193  44908  disjxp1  45429  dmrelrnrel  45584  infleinflem2  45729  mullimc  45976  mullimcf  45983  addlimc  46006  0ellimcdiv  46007  icccncfext  46245  stoweidlem52  46410  wallispilem4  46426  fourierdlem16  46481  fourierdlem21  46486  fourierdlem48  46512  fourierdlem51  46515  fourierdlem52  46516  fourierdlem54  46518  fourierdlem64  46528  fourierdlem76  46540  fourierdlem77  46541  fourierdlem80  46544  fourierdlem86  46550  fourierdlem87  46551  fourierdlem102  46566  fourierdlem114  46578  sge0f1o  46740  sge0split  46767  nnfoctbdjlem  46813  iundjiun  46818  ismeannd  46825  psmeasure  46829  isomennd  46889  hoidmvle  46958  ovncvr2  46969  dfatbrafv2b  47605  oexpnegnz  48038  clnbgrgrim  48294  usgrexmpl2trifr  48397  rngcinvALTV  48636  ringcinvALTV  48670  itsclc0b  49132  seposep  49285