Theorem jca31 516

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 513	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		jca31.3	. 2 ⊢ (𝜑 → 𝜃)
5	3, 4	jca 513	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  3jca  1128  syl21anbrc  1344  xpdifid  6086  tpres  7108  f1oiso2  7255  oewordri  8454  boxriin  8759  cantnfrescl  9478  cfsuc  10059  prsrlem1  10874  lemulge11  11883  lediv12a  11914  elnnz  12375  quoremz  13621  quoremnn0ALT  13623  fldiv  13626  modsumfzodifsn  13710  leexp1a  13939  faclbnd6  14059  wrdlen2i  14700  wwlktovfo  14718  setcinv  17850  sgrp2rid2  18610  grpidinv2  18679  gsumval3lem1  19551  dvdsrzring  20728  cncnp2  22477  vitalilem1  24817  aaliou3lem2  25548  2sqreulem1  26639  2sqreunnlem1  26642  pntibndlem2  26784  tgjustf  26879  iscgrglt  26920  islnoppd  27146  oppcom  27150  opphllem1  27153  opphllem5  27157  oppperpex  27159  hpgerlem  27171  colhp  27176  ax5seg  27351  uhgr2edg  27620  nbupgrres  27776  usgr2pthlem  28176  crctcshwlkn0lem5  28224  clwwlknonwwlknonb  28515  1pthond  28553  3pthdlem1  28573  frgrwopreglem5a  28720  grpoidinv  28915  nmcvcn  29102  leopmul  30541  resf1o  31110  trsp2cyc  31435  rhmopp  31563  oddpwdc  32366  poseq  33847  btwnconn1  34448  finminlem  34552  ptrecube  35821  poimirlem22  35843  isrngod  36100  paddasslem4  37879  cdleme21h  38390  cdleme26eALTN  38417  cdleme40m  38523  cdlemf2  38618  dicssdvh  39242  dihopelvalcpre  39304  dihmeetlem4preN  39362  dih1dimatlem0  39384  sticksstones22  40166  metakunt17  40183  lzenom  40629  jm2.27c  40867  clrellem  41268  2pm13.193  42210  disjxp1  42655  dmrelrnrel  42810  infleinflem2  42958  mullimc  43206  mullimcf  43213  addlimc  43238  0ellimcdiv  43239  icccncfext  43477  stoweidlem52  43642  wallispilem4  43658  fourierdlem16  43713  fourierdlem21  43718  fourierdlem48  43744  fourierdlem51  43747  fourierdlem52  43748  fourierdlem54  43750  fourierdlem64  43760  fourierdlem76  43772  fourierdlem77  43773  fourierdlem80  43776  fourierdlem86  43782  fourierdlem87  43783  fourierdlem102  43798  fourierdlem114  43810  sge0f1o  43970  sge0split  43997  nnfoctbdjlem  44043  iundjiun  44048  ismeannd  44055  psmeasure  44059  isomennd  44119  hoidmvle  44188  ovncvr2  44199  dfatbrafv2b  44795  oexpnegnz  45188  rngcinv  45597  rngcinvALTV  45609  ringcinv  45648  ringcinvALTV  45672  itsclc0b  46176  seposep  46277