Theorem jca31 513

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  3jca  1125  syl21anbrc  1341  xpdifid  6179  tpres  7218  f1oiso2  7364  poseq  8172  oewordri  8622  boxriin  8969  cantnfrescl  9719  cfsuc  10300  prsrlem1  11115  lemulge11  12128  lediv12a  12159  elnnz  12620  quoremz  13875  quoremnn0ALT  13877  fldiv  13880  modsumfzodifsn  13964  leexp1a  14194  faclbnd6  14316  wrdlen2i  14951  wwlktovfo  14967  setcinv  18112  sgrp2rid2  18916  grpidinv2  18992  eqg0subg  19190  gsumval3lem1  19903  rhmopp  20491  rngcinv  20615  ringcinv  20649  dvdsrzring  21451  cncnp2  23276  vitalilem1  25628  aaliou3lem2  26371  2sqreulem1  27475  2sqreunnlem1  27478  pntibndlem2  27620  tgjustf  28400  iscgrglt  28441  islnoppd  28667  oppcom  28671  opphllem1  28674  opphllem5  28678  oppperpex  28680  hpgerlem  28692  colhp  28697  ax5seg  28872  uhgr2edg  29144  nbupgrres  29300  usgr2pthlem  29700  crctcshwlkn0lem5  29748  clwwlknonwwlknonb  30039  1pthond  30077  3pthdlem1  30097  frgrwopreglem5a  30244  grpoidinv  30441  nmcvcn  30628  leopmul  32067  resf1o  32644  trsp2cyc  33001  oddpwdc  34188  btwnconn1  35925  finminlem  36030  ptrecube  37321  poimirlem22  37343  isrngod  37599  paddasslem4  39522  cdleme21h  40033  cdleme26eALTN  40060  cdleme40m  40166  cdlemf2  40261  dicssdvh  40885  dihopelvalcpre  40947  dihmeetlem4preN  41005  dih1dimatlem0  41027  primrootscoprmpow  41797  primrootscoprbij  41800  aks6d1c5  41837  sticksstones22  41866  aks6d1c6lem3  41870  metakunt17  41907  lzenom  42427  jm2.27c  42665  omltoe  43074  clrellem  43289  2pm13.193  44228  disjxp1  44670  dmrelrnrel  44833  infleinflem2  44986  mullimc  45237  mullimcf  45244  addlimc  45269  0ellimcdiv  45270  icccncfext  45508  stoweidlem52  45673  wallispilem4  45689  fourierdlem16  45744  fourierdlem21  45749  fourierdlem48  45775  fourierdlem51  45778  fourierdlem52  45779  fourierdlem54  45781  fourierdlem64  45791  fourierdlem76  45803  fourierdlem77  45804  fourierdlem80  45807  fourierdlem86  45813  fourierdlem87  45814  fourierdlem102  45829  fourierdlem114  45841  sge0f1o  46003  sge0split  46030  nnfoctbdjlem  46076  iundjiun  46081  ismeannd  46088  psmeasure  46092  isomennd  46152  hoidmvle  46221  ovncvr2  46232  dfatbrafv2b  46858  oexpnegnz  47250  clnbgrgrim  47481  rngcinvALTV  47653  ringcinvALTV  47687  itsclc0b  48160  seposep  48259