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  6160  xpdifcnvepel  6161  tpres  7200  f1oiso2  7353  poseq  8156  oewordri  8580  boxriin  8947  cantnfrescl  9655  cfsuc  10259  prsrlem1  11081  lemulge11  12101  lediv12a  12132  elnnz  12625  quoremz  13916  quoremnn0ALT  13918  fldiv  13921  modsumfzodifsn  14008  leexp1a  14239  faclbnd6  14363  wrdlen2i  15013  wwlktovfo  15031  setcinv  18179  sgrp2rid2  19038  grpidinv2  19121  eqg0subg  19324  gsumval3lem1  20032  rhmopp  20669  rngcinv  20799  ringcinv  20833  dvdsrzring  21674  cncnp2  23506  vitalilem1  25836  aaliou3lem2  26579  2sqreulem1  27682  2sqreunnlem1  27685  pntibndlem2  27827  elnnzs  28666  tgjustf  28814  iscgrglt  28856  islnoppd  29095  oppcom  29099  opphllem1  29102  opphllem5  29106  oppperpex  29108  hpgerlem  29122  colhp  29127  prlngsym  29298  ax5seg  29395  uhgr2edg  29668  nbupgrres  29824  usgr2pthlem  30228  crctcshwlkn0lem5  30282  clwwlknonwwlknonb  30576  1pthond  30614  3pthdlem1  30644  frgrwopreglem5a  30791  grpoidinv  30989  nmcvcn  31176  leopmul  32615  resf1o  33201  trsp2cyc  33563  oddpwdc  34865  btwnconn1  36681  finminlem  36937  ptrecube  38369  poimirlem22  38391  isrngod  38648  paddasslem4  40696  cdleme21h  41207  cdleme26eALTN  41234  cdleme40m  41340  cdlemf2  41435  dicssdvh  42059  dihopelvalcpre  42121  dihmeetlem4preN  42179  dih1dimatlem0  42201  primrootscoprmpow  42965  primrootscoprbij  42968  aks6d1c5  43005  sticksstones22  43034  aks6d1c6lem3  43038  unitscyglem3  43063  unitscyglem5  43065  lzenom  43615  jm2.27c  43848  omltoe  44247  clrellem  44462  2pm13.193  45375  disjxp1  45903  dmrelrnrel  46056  infleinflem2  46200  mullimc  46446  mullimcf  46453  addlimc  46476  0ellimcdiv  46477  icccncfext  46715  stoweidlem52  46880  wallispilem4  46896  fourierdlem16  46951  fourierdlem21  46956  fourierdlem48  46982  fourierdlem51  46985  fourierdlem52  46986  fourierdlem54  46988  fourierdlem64  46998  fourierdlem76  47010  fourierdlem77  47011  fourierdlem80  47014  fourierdlem86  47020  fourierdlem87  47021  fourierdlem102  47036  fourierdlem114  47048  sge0f1o  47210  sge0split  47237  nnfoctbdjlem  47283  iundjiun  47288  ismeannd  47295  psmeasure  47299  isomennd  47359  hoidmvle  47428  ovncvr2  47439  dfatbrafv2b  48133  oexpnegnz  48594  clnbgrgrim  48850  usgrexmpl2trifr  48953  rngcinvALTV  49191  ringcinvALTV  49225  itsclc0b  49702  seposep  49852