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  6157  tpres  7192  f1oiso2  7344  poseq  8155  oewordri  8602  boxriin  8952  cantnfrescl  9688  cfsuc  10269  prsrlem1  11084  lemulge11  12102  lediv12a  12133  elnnz  12596  quoremz  13870  quoremnn0ALT  13872  fldiv  13875  modsumfzodifsn  13960  leexp1a  14191  faclbnd6  14315  wrdlen2i  14959  wwlktovfo  14975  setcinv  18101  sgrp2rid2  18902  grpidinv2  18978  eqg0subg  19177  gsumval3lem1  19884  rhmopp  20467  rngcinv  20595  ringcinv  20629  dvdsrzring  21420  cncnp2  23217  vitalilem1  25559  aaliou3lem2  26301  2sqreulem1  27407  2sqreunnlem1  27410  pntibndlem2  27552  elnnzs  28304  tgjustf  28398  iscgrglt  28439  islnoppd  28665  oppcom  28669  opphllem1  28672  opphllem5  28676  oppperpex  28678  hpgerlem  28690  colhp  28695  ax5seg  28863  uhgr2edg  29133  nbupgrres  29289  usgr2pthlem  29691  crctcshwlkn0lem5  29742  clwwlknonwwlknonb  30033  1pthond  30071  3pthdlem1  30091  frgrwopreglem5a  30238  grpoidinv  30435  nmcvcn  30622  leopmul  32061  resf1o  32653  trsp2cyc  33080  oddpwdc  34332  btwnconn1  36065  finminlem  36282  ptrecube  37590  poimirlem22  37612  isrngod  37868  paddasslem4  39788  cdleme21h  40299  cdleme26eALTN  40326  cdleme40m  40432  cdlemf2  40527  dicssdvh  41151  dihopelvalcpre  41213  dihmeetlem4preN  41271  dih1dimatlem0  41293  primrootscoprmpow  42058  primrootscoprbij  42061  aks6d1c5  42098  sticksstones22  42127  aks6d1c6lem3  42131  unitscyglem3  42156  unitscyglem5  42158  metakunt17  42180  lzenom  42740  jm2.27c  42978  omltoe  43378  clrellem  43593  2pm13.193  44525  disjxp1  45041  dmrelrnrel  45198  infleinflem2  45346  mullimc  45593  mullimcf  45600  addlimc  45625  0ellimcdiv  45626  icccncfext  45864  stoweidlem52  46029  wallispilem4  46045  fourierdlem16  46100  fourierdlem21  46105  fourierdlem48  46131  fourierdlem51  46134  fourierdlem52  46135  fourierdlem54  46137  fourierdlem64  46147  fourierdlem76  46159  fourierdlem77  46160  fourierdlem80  46163  fourierdlem86  46169  fourierdlem87  46170  fourierdlem102  46185  fourierdlem114  46197  sge0f1o  46359  sge0split  46386  nnfoctbdjlem  46432  iundjiun  46437  ismeannd  46444  psmeasure  46448  isomennd  46508  hoidmvle  46577  ovncvr2  46588  dfatbrafv2b  47222  oexpnegnz  47640  clnbgrgrim  47895  usgrexmpl2trifr  47989  rngcinvALTV  48199  ringcinvALTV  48233  itsclc0b  48700  seposep  48848