Theorem jca31 515

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  3jca  1127  syl21anbrc  1343  xpdifid  6064  tpres  7068  f1oiso2  7215  oewordri  8410  boxriin  8715  cantnfrescl  9421  cfsuc  10023  prsrlem1  10838  lemulge11  11847  lediv12a  11878  elnnz  12339  quoremz  13585  quoremnn0ALT  13587  fldiv  13590  modsumfzodifsn  13674  leexp1a  13903  faclbnd6  14023  wrdlen2i  14665  wwlktovfo  14683  setcinv  17815  sgrp2rid2  18575  grpidinv2  18644  gsumval3lem1  19516  dvdsrzring  20693  cncnp2  22442  vitalilem1  24782  aaliou3lem2  25513  2sqreulem1  26604  2sqreunnlem1  26607  pntibndlem2  26749  tgjustf  26844  iscgrglt  26885  islnoppd  27111  oppcom  27115  opphllem1  27118  opphllem5  27122  oppperpex  27124  hpgerlem  27136  colhp  27141  ax5seg  27316  uhgr2edg  27585  nbupgrres  27741  usgr2pthlem  28139  crctcshwlkn0lem5  28187  clwwlknonwwlknonb  28478  1pthond  28516  3pthdlem1  28536  frgrwopreglem5a  28683  grpoidinv  28878  nmcvcn  29065  leopmul  30504  resf1o  31073  trsp2cyc  31398  rhmopp  31526  oddpwdc  32329  poseq  33810  btwnconn1  34411  finminlem  34515  ptrecube  35785  poimirlem22  35807  isrngod  36064  paddasslem4  37845  cdleme21h  38356  cdleme26eALTN  38383  cdleme40m  38489  cdlemf2  38584  dicssdvh  39208  dihopelvalcpre  39270  dihmeetlem4preN  39328  dih1dimatlem0  39350  sticksstones22  40132  metakunt17  40149  lzenom  40600  jm2.27c  40837  clrellem  41211  2pm13.193  42153  disjxp1  42598  dmrelrnrel  42746  infleinflem2  42891  mullimc  43138  mullimcf  43145  addlimc  43170  0ellimcdiv  43171  icccncfext  43409  stoweidlem52  43574  wallispilem4  43590  fourierdlem16  43645  fourierdlem21  43650  fourierdlem48  43676  fourierdlem51  43679  fourierdlem52  43680  fourierdlem54  43682  fourierdlem64  43692  fourierdlem76  43704  fourierdlem77  43705  fourierdlem80  43708  fourierdlem86  43714  fourierdlem87  43715  fourierdlem102  43730  fourierdlem114  43742  sge0f1o  43901  sge0split  43928  nnfoctbdjlem  43974  iundjiun  43979  ismeannd  43986  psmeasure  43990  isomennd  44050  hoidmvle  44119  ovncvr2  44130  dfatbrafv2b  44715  oexpnegnz  45108  rngcinv  45517  rngcinvALTV  45529  ringcinv  45568  ringcinvALTV  45592  itsclc0b  46096  seposep  46197