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  6143  tpres  7177  f1oiso2  7329  poseq  8139  oewordri  8558  boxriin  8915  cantnfrescl  9635  cfsuc  10216  prsrlem1  11031  lemulge11  12051  lediv12a  12082  elnnz  12545  quoremz  13823  quoremnn0ALT  13825  fldiv  13828  modsumfzodifsn  13915  leexp1a  14146  faclbnd6  14270  wrdlen2i  14914  wwlktovfo  14930  setcinv  18058  sgrp2rid2  18859  grpidinv2  18935  eqg0subg  19134  gsumval3lem1  19841  rhmopp  20424  rngcinv  20552  ringcinv  20586  dvdsrzring  21377  cncnp2  23174  vitalilem1  25515  aaliou3lem2  26257  2sqreulem1  27363  2sqreunnlem1  27366  pntibndlem2  27508  elnnzs  28295  tgjustf  28406  iscgrglt  28447  islnoppd  28673  oppcom  28677  opphllem1  28680  opphllem5  28684  oppperpex  28686  hpgerlem  28698  colhp  28703  ax5seg  28871  uhgr2edg  29141  nbupgrres  29297  usgr2pthlem  29699  crctcshwlkn0lem5  29750  clwwlknonwwlknonb  30041  1pthond  30079  3pthdlem1  30099  frgrwopreglem5a  30246  grpoidinv  30443  nmcvcn  30630  leopmul  32069  resf1o  32659  trsp2cyc  33086  oddpwdc  34351  btwnconn1  36084  finminlem  36301  ptrecube  37609  poimirlem22  37631  isrngod  37887  paddasslem4  39812  cdleme21h  40323  cdleme26eALTN  40350  cdleme40m  40456  cdlemf2  40551  dicssdvh  41175  dihopelvalcpre  41237  dihmeetlem4preN  41295  dih1dimatlem0  41317  primrootscoprmpow  42082  primrootscoprbij  42085  aks6d1c5  42122  sticksstones22  42151  aks6d1c6lem3  42155  unitscyglem3  42180  unitscyglem5  42182  lzenom  42751  jm2.27c  42989  omltoe  43389  clrellem  43604  2pm13.193  44535  disjxp1  45056  dmrelrnrel  45213  infleinflem2  45360  mullimc  45607  mullimcf  45614  addlimc  45639  0ellimcdiv  45640  icccncfext  45878  stoweidlem52  46043  wallispilem4  46059  fourierdlem16  46114  fourierdlem21  46119  fourierdlem48  46145  fourierdlem51  46148  fourierdlem52  46149  fourierdlem54  46151  fourierdlem64  46161  fourierdlem76  46173  fourierdlem77  46174  fourierdlem80  46177  fourierdlem86  46183  fourierdlem87  46184  fourierdlem102  46199  fourierdlem114  46211  sge0f1o  46373  sge0split  46400  nnfoctbdjlem  46446  iundjiun  46451  ismeannd  46458  psmeasure  46462  isomennd  46522  hoidmvle  46591  ovncvr2  46602  dfatbrafv2b  47236  oexpnegnz  47669  clnbgrgrim  47924  usgrexmpl2trifr  48018  rngcinvALTV  48254  ringcinvALTV  48288  itsclc0b  48751  seposep  48902