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  6144  tpres  7178  f1oiso2  7330  poseq  8140  oewordri  8559  boxriin  8916  cantnfrescl  9636  cfsuc  10217  prsrlem1  11032  lemulge11  12052  lediv12a  12083  elnnz  12546  quoremz  13824  quoremnn0ALT  13826  fldiv  13829  modsumfzodifsn  13916  leexp1a  14147  faclbnd6  14271  wrdlen2i  14915  wwlktovfo  14931  setcinv  18059  sgrp2rid2  18860  grpidinv2  18936  eqg0subg  19135  gsumval3lem1  19842  rhmopp  20425  rngcinv  20553  ringcinv  20587  dvdsrzring  21378  cncnp2  23175  vitalilem1  25516  aaliou3lem2  26258  2sqreulem1  27364  2sqreunnlem1  27367  pntibndlem2  27509  elnnzs  28296  tgjustf  28407  iscgrglt  28448  islnoppd  28674  oppcom  28678  opphllem1  28681  opphllem5  28685  oppperpex  28687  hpgerlem  28699  colhp  28704  ax5seg  28872  uhgr2edg  29142  nbupgrres  29298  usgr2pthlem  29700  crctcshwlkn0lem5  29751  clwwlknonwwlknonb  30042  1pthond  30080  3pthdlem1  30100  frgrwopreglem5a  30247  grpoidinv  30444  nmcvcn  30631  leopmul  32070  resf1o  32660  trsp2cyc  33087  oddpwdc  34352  btwnconn1  36096  finminlem  36313  ptrecube  37621  poimirlem22  37643  isrngod  37899  paddasslem4  39824  cdleme21h  40335  cdleme26eALTN  40362  cdleme40m  40468  cdlemf2  40563  dicssdvh  41187  dihopelvalcpre  41249  dihmeetlem4preN  41307  dih1dimatlem0  41329  primrootscoprmpow  42094  primrootscoprbij  42097  aks6d1c5  42134  sticksstones22  42163  aks6d1c6lem3  42167  unitscyglem3  42192  unitscyglem5  42194  lzenom  42765  jm2.27c  43003  omltoe  43403  clrellem  43618  2pm13.193  44549  disjxp1  45070  dmrelrnrel  45227  infleinflem2  45374  mullimc  45621  mullimcf  45628  addlimc  45653  0ellimcdiv  45654  icccncfext  45892  stoweidlem52  46057  wallispilem4  46073  fourierdlem16  46128  fourierdlem21  46133  fourierdlem48  46159  fourierdlem51  46162  fourierdlem52  46163  fourierdlem54  46165  fourierdlem64  46175  fourierdlem76  46187  fourierdlem77  46188  fourierdlem80  46191  fourierdlem86  46197  fourierdlem87  46198  fourierdlem102  46213  fourierdlem114  46225  sge0f1o  46387  sge0split  46414  nnfoctbdjlem  46460  iundjiun  46465  ismeannd  46472  psmeasure  46476  isomennd  46536  hoidmvle  46605  ovncvr2  46616  dfatbrafv2b  47250  oexpnegnz  47683  clnbgrgrim  47938  usgrexmpl2trifr  48032  rngcinvALTV  48268  ringcinvALTV  48302  itsclc0b  48765  seposep  48918