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  6132  tpres  7156  f1oiso2  7307  poseq  8108  oewordri  8528  boxriin  8888  cantnfrescl  9597  cfsuc  10179  prsrlem1  10995  lemulge11  12018  lediv12a  12049  elnnz  12534  quoremz  13814  quoremnn0ALT  13816  fldiv  13819  modsumfzodifsn  13906  leexp1a  14137  faclbnd6  14261  wrdlen2i  14904  wwlktovfo  14920  setcinv  18057  sgrp2rid2  18897  grpidinv2  18973  eqg0subg  19171  gsumval3lem1  19880  rhmopp  20486  rngcinv  20614  ringcinv  20648  dvdsrzring  21441  cncnp2  23246  vitalilem1  25575  aaliou3lem2  26309  2sqreulem1  27409  2sqreunnlem1  27412  pntibndlem2  27554  elnnzs  28393  tgjustf  28541  iscgrglt  28582  islnoppd  28808  oppcom  28812  opphllem1  28815  opphllem5  28819  oppperpex  28821  hpgerlem  28833  colhp  28838  ax5seg  29007  uhgr2edg  29277  nbupgrres  29433  usgr2pthlem  29831  crctcshwlkn0lem5  29882  clwwlknonwwlknonb  30176  1pthond  30214  3pthdlem1  30234  frgrwopreglem5a  30381  grpoidinv  30579  nmcvcn  30766  leopmul  32205  resf1o  32803  trsp2cyc  33184  oddpwdc  34498  btwnconn1  36283  finminlem  36500  ptrecube  37941  poimirlem22  37963  isrngod  38219  paddasslem4  40269  cdleme21h  40780  cdleme26eALTN  40807  cdleme40m  40913  cdlemf2  41008  dicssdvh  41632  dihopelvalcpre  41694  dihmeetlem4preN  41752  dih1dimatlem0  41774  primrootscoprmpow  42538  primrootscoprbij  42541  aks6d1c5  42578  sticksstones22  42607  aks6d1c6lem3  42611  unitscyglem3  42636  unitscyglem5  42638  lzenom  43202  jm2.27c  43435  omltoe  43834  clrellem  44049  2pm13.193  44979  disjxp1  45500  dmrelrnrel  45655  infleinflem2  45800  mullimc  46046  mullimcf  46053  addlimc  46076  0ellimcdiv  46077  icccncfext  46315  stoweidlem52  46480  wallispilem4  46496  fourierdlem16  46551  fourierdlem21  46556  fourierdlem48  46582  fourierdlem51  46585  fourierdlem52  46586  fourierdlem54  46588  fourierdlem64  46598  fourierdlem76  46610  fourierdlem77  46611  fourierdlem80  46614  fourierdlem86  46620  fourierdlem87  46621  fourierdlem102  46636  fourierdlem114  46648  sge0f1o  46810  sge0split  46837  nnfoctbdjlem  46883  iundjiun  46888  ismeannd  46895  psmeasure  46899  isomennd  46959  hoidmvle  47028  ovncvr2  47039  dfatbrafv2b  47693  oexpnegnz  48154  clnbgrgrim  48410  usgrexmpl2trifr  48513  rngcinvALTV  48752  ringcinvALTV  48786  itsclc0b  49248  seposep  49401