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  6158  xpdifcnvepel  6159  tpres  7207  f1oiso2  7360  poseq  8175  oewordri  8601  boxriin  8968  cantnfrescl  9677  cfsuc  10335  prsrlem1  11157  lemulge11  12179  lediv12a  12210  elnnz  12703  quoremz  13995  quoremnn0ALT  13997  fldiv  14000  modsumfzodifsn  14087  leexp1a  14318  faclbnd6  14443  wrdlen2i  15093  wwlktovfo  15111  setcinv  18265  sgrp2rid2  19125  grpidinv2  19208  eqg0subg  19411  gsumval3lem1  20119  rhmopp  20759  rngcinv  20889  ringcinv  20923  dvdsrzring  21767  cncnp2  23599  vitalilem1  25929  aaliou3lem2  26670  2sqreulem1  27773  2sqreunnlem1  27776  pntibndlem2  27918  elnnzs  28787  tgjustf  28935  iscgrglt  28977  islnoppd  29216  oppcom  29220  opphllem1  29223  opphllem5  29227  oppperpex  29229  hpgerlem  29243  colhp  29248  prlngsym  29419  ax5seg  29516  uhgr2edg  29789  nbupgrres  29945  usgr2pthlem  30349  crctcshwlkn0lem5  30403  clwwlknonwwlknonb  30697  1pthond  30735  3pthdlem1  30765  frgrwopreglem5a  30912  grpoidinv  31110  nmcvcn  31297  leopmul  32736  resf1o  33322  trsp2cyc  33684  oddpwdc  34986  btwnconn1  36866  finminlem  37106  ptrecube  38539  poimirlem22  38561  isrngod  38833  paddasslem4  40881  cdleme21h  41392  cdleme26eALTN  41419  cdleme40m  41525  cdlemf2  41620  dicssdvh  42244  dihopelvalcpre  42306  dihmeetlem4preN  42364  dih1dimatlem0  42386  primrootscoprmpow  43150  primrootscoprbij  43153  aks6d1c5  43190  sticksstones22  43219  aks6d1c6lem3  43223  unitscyglem3  43248  unitscyglem5  43250  lzenom  43781  jm2.27c  44014  omltoe  44408  clrellem  44622  2pm13.193  45535  disjxp1  46086  dmrelrnrel  46239  infleinflem2  46382  mullimc  46628  mullimcf  46635  addlimc  46658  0ellimcdiv  46659  icccncfext  46897  stoweidlem52  47062  wallispilem4  47078  fourierdlem16  47133  fourierdlem21  47138  fourierdlem48  47164  fourierdlem51  47167  fourierdlem52  47168  fourierdlem54  47170  fourierdlem64  47180  fourierdlem76  47192  fourierdlem77  47193  fourierdlem80  47196  fourierdlem86  47202  fourierdlem87  47203  fourierdlem102  47218  fourierdlem114  47230  sge0f1o  47392  sge0split  47419  nnfoctbdjlem  47465  iundjiun  47470  ismeannd  47477  psmeasure  47481  isomennd  47541  hoidmvle  47610  ovncvr2  47621  dfatbrafv2b  48315  oexpnegnz  48776  clnbgrgrim  49032  usgrexmpl2trifr  49135  rngcinvALTV  49373  ringcinvALTV  49407  itsclc0b  49884  seposep  50034