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  1127  syl21anbrc  1343  xpdifid  6189  tpres  7220  f1oiso2  7371  poseq  8181  oewordri  8628  boxriin  8978  cantnfrescl  9713  cfsuc  10294  prsrlem1  11109  lemulge11  12127  lediv12a  12158  elnnz  12620  quoremz  13891  quoremnn0ALT  13893  fldiv  13896  modsumfzodifsn  13981  leexp1a  14211  faclbnd6  14334  wrdlen2i  14977  wwlktovfo  14993  setcinv  18143  sgrp2rid2  18951  grpidinv2  19027  eqg0subg  19226  gsumval3lem1  19937  rhmopp  20525  rngcinv  20653  ringcinv  20687  dvdsrzring  21489  cncnp2  23304  vitalilem1  25656  aaliou3lem2  26399  2sqreulem1  27504  2sqreunnlem1  27507  pntibndlem2  27649  elnnzs  28401  tgjustf  28495  iscgrglt  28536  islnoppd  28762  oppcom  28766  opphllem1  28769  opphllem5  28773  oppperpex  28775  hpgerlem  28787  colhp  28792  ax5seg  28967  uhgr2edg  29239  nbupgrres  29395  usgr2pthlem  29795  crctcshwlkn0lem5  29843  clwwlknonwwlknonb  30134  1pthond  30172  3pthdlem1  30192  frgrwopreglem5a  30339  grpoidinv  30536  nmcvcn  30723  leopmul  32162  resf1o  32747  trsp2cyc  33125  oddpwdc  34335  btwnconn1  36082  finminlem  36300  ptrecube  37606  poimirlem22  37628  isrngod  37884  paddasslem4  39805  cdleme21h  40316  cdleme26eALTN  40343  cdleme40m  40449  cdlemf2  40544  dicssdvh  41168  dihopelvalcpre  41230  dihmeetlem4preN  41288  dih1dimatlem0  41310  primrootscoprmpow  42080  primrootscoprbij  42083  aks6d1c5  42120  sticksstones22  42149  aks6d1c6lem3  42153  unitscyglem3  42178  unitscyglem5  42180  metakunt17  42202  lzenom  42757  jm2.27c  42995  omltoe  43396  clrellem  43611  2pm13.193  44549  disjxp1  45008  dmrelrnrel  45168  infleinflem2  45320  mullimc  45571  mullimcf  45578  addlimc  45603  0ellimcdiv  45604  icccncfext  45842  stoweidlem52  46007  wallispilem4  46023  fourierdlem16  46078  fourierdlem21  46083  fourierdlem48  46109  fourierdlem51  46112  fourierdlem52  46113  fourierdlem54  46115  fourierdlem64  46125  fourierdlem76  46137  fourierdlem77  46138  fourierdlem80  46141  fourierdlem86  46147  fourierdlem87  46148  fourierdlem102  46163  fourierdlem114  46175  sge0f1o  46337  sge0split  46364  nnfoctbdjlem  46410  iundjiun  46415  ismeannd  46422  psmeasure  46426  isomennd  46486  hoidmvle  46555  ovncvr2  46566  dfatbrafv2b  47194  oexpnegnz  47602  clnbgrgrim  47839  usgrexmpl2trifr  47931  rngcinvALTV  48119  ringcinvALTV  48153  itsclc0b  48621  seposep  48721