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  1345  xpdifid  6188  tpres  7221  f1oiso2  7372  poseq  8183  oewordri  8630  boxriin  8980  cantnfrescl  9716  cfsuc  10297  prsrlem1  11112  lemulge11  12130  lediv12a  12161  elnnz  12623  quoremz  13895  quoremnn0ALT  13897  fldiv  13900  modsumfzodifsn  13985  leexp1a  14215  faclbnd6  14338  wrdlen2i  14981  wwlktovfo  14997  setcinv  18135  sgrp2rid2  18939  grpidinv2  19015  eqg0subg  19214  gsumval3lem1  19923  rhmopp  20509  rngcinv  20637  ringcinv  20671  dvdsrzring  21472  cncnp2  23289  vitalilem1  25643  aaliou3lem2  26385  2sqreulem1  27490  2sqreunnlem1  27493  pntibndlem2  27635  elnnzs  28387  tgjustf  28481  iscgrglt  28522  islnoppd  28748  oppcom  28752  opphllem1  28755  opphllem5  28759  oppperpex  28761  hpgerlem  28773  colhp  28778  ax5seg  28953  uhgr2edg  29225  nbupgrres  29381  usgr2pthlem  29783  crctcshwlkn0lem5  29834  clwwlknonwwlknonb  30125  1pthond  30163  3pthdlem1  30183  frgrwopreglem5a  30330  grpoidinv  30527  nmcvcn  30714  leopmul  32153  resf1o  32741  trsp2cyc  33143  oddpwdc  34356  btwnconn1  36102  finminlem  36319  ptrecube  37627  poimirlem22  37649  isrngod  37905  paddasslem4  39825  cdleme21h  40336  cdleme26eALTN  40363  cdleme40m  40469  cdlemf2  40564  dicssdvh  41188  dihopelvalcpre  41250  dihmeetlem4preN  41308  dih1dimatlem0  41330  primrootscoprmpow  42100  primrootscoprbij  42103  aks6d1c5  42140  sticksstones22  42169  aks6d1c6lem3  42173  unitscyglem3  42198  unitscyglem5  42200  metakunt17  42222  lzenom  42781  jm2.27c  43019  omltoe  43420  clrellem  43635  2pm13.193  44572  disjxp1  45074  dmrelrnrel  45231  infleinflem2  45382  mullimc  45631  mullimcf  45638  addlimc  45663  0ellimcdiv  45664  icccncfext  45902  stoweidlem52  46067  wallispilem4  46083  fourierdlem16  46138  fourierdlem21  46143  fourierdlem48  46169  fourierdlem51  46172  fourierdlem52  46173  fourierdlem54  46175  fourierdlem64  46185  fourierdlem76  46197  fourierdlem77  46198  fourierdlem80  46201  fourierdlem86  46207  fourierdlem87  46208  fourierdlem102  46223  fourierdlem114  46235  sge0f1o  46397  sge0split  46424  nnfoctbdjlem  46470  iundjiun  46475  ismeannd  46482  psmeasure  46486  isomennd  46546  hoidmvle  46615  ovncvr2  46626  dfatbrafv2b  47257  oexpnegnz  47665  clnbgrgrim  47902  usgrexmpl2trifr  47996  rngcinvALTV  48192  ringcinvALTV  48226  itsclc0b  48693  seposep  48823