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  6129  tpres  7157  f1oiso2  7309  poseq  8114  oewordri  8533  boxriin  8890  cantnfrescl  9605  cfsuc  10186  prsrlem1  11001  lemulge11  12021  lediv12a  12052  elnnz  12515  quoremz  13793  quoremnn0ALT  13795  fldiv  13798  modsumfzodifsn  13885  leexp1a  14116  faclbnd6  14240  wrdlen2i  14884  wwlktovfo  14900  setcinv  18028  sgrp2rid2  18829  grpidinv2  18905  eqg0subg  19104  gsumval3lem1  19811  rhmopp  20394  rngcinv  20522  ringcinv  20556  dvdsrzring  21347  cncnp2  23144  vitalilem1  25485  aaliou3lem2  26227  2sqreulem1  27333  2sqreunnlem1  27336  pntibndlem2  27478  elnnzs  28265  tgjustf  28376  iscgrglt  28417  islnoppd  28643  oppcom  28647  opphllem1  28650  opphllem5  28654  oppperpex  28656  hpgerlem  28668  colhp  28673  ax5seg  28841  uhgr2edg  29111  nbupgrres  29267  usgr2pthlem  29666  crctcshwlkn0lem5  29717  clwwlknonwwlknonb  30008  1pthond  30046  3pthdlem1  30066  frgrwopreglem5a  30213  grpoidinv  30410  nmcvcn  30597  leopmul  32036  resf1o  32626  trsp2cyc  33053  oddpwdc  34318  btwnconn1  36062  finminlem  36279  ptrecube  37587  poimirlem22  37609  isrngod  37865  paddasslem4  39790  cdleme21h  40301  cdleme26eALTN  40328  cdleme40m  40434  cdlemf2  40529  dicssdvh  41153  dihopelvalcpre  41215  dihmeetlem4preN  41273  dih1dimatlem0  41295  primrootscoprmpow  42060  primrootscoprbij  42063  aks6d1c5  42100  sticksstones22  42129  aks6d1c6lem3  42133  unitscyglem3  42158  unitscyglem5  42160  lzenom  42731  jm2.27c  42969  omltoe  43369  clrellem  43584  2pm13.193  44515  disjxp1  45036  dmrelrnrel  45193  infleinflem2  45340  mullimc  45587  mullimcf  45594  addlimc  45619  0ellimcdiv  45620  icccncfext  45858  stoweidlem52  46023  wallispilem4  46039  fourierdlem16  46094  fourierdlem21  46099  fourierdlem48  46125  fourierdlem51  46128  fourierdlem52  46129  fourierdlem54  46131  fourierdlem64  46141  fourierdlem76  46153  fourierdlem77  46154  fourierdlem80  46157  fourierdlem86  46163  fourierdlem87  46164  fourierdlem102  46179  fourierdlem114  46191  sge0f1o  46353  sge0split  46380  nnfoctbdjlem  46426  iundjiun  46431  ismeannd  46438  psmeasure  46442  isomennd  46502  hoidmvle  46571  ovncvr2  46582  dfatbrafv2b  47219  oexpnegnz  47652  clnbgrgrim  47907  usgrexmpl2trifr  48001  rngcinvALTV  48237  ringcinvALTV  48271  itsclc0b  48734  seposep  48887