Theorem jca31 519

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 516	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		jca31.3	. 2 ⊢ (𝜑 → 𝜃)
5	3, 4	jca 516	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 208  df-an 397

This theorem is referenced by:  3jca  1134  syl21anbrc  1351  xpdifid  6119  tpres  7145  f1oiso2  7296  poseq  8098  oewordri  8518  boxriin  8878  cantnfrescl  9588  cfsuc  10170  prsrlem1  10986  lemulge11  12009  lediv12a  12040  elnnz  12525  quoremz  13805  quoremnn0ALT  13807  fldiv  13810  modsumfzodifsn  13897  leexp1a  14128  faclbnd6  14252  wrdlen2i  14895  wwlktovfo  14911  setcinv  18048  sgrp2rid2  18888  grpidinv2  18964  eqg0subg  19162  gsumval3lem1  19871  rhmopp  20481  rngcinv  20609  ringcinv  20643  dvdsrzring  21436  cncnp2  23264  vitalilem1  25593  aaliou3lem2  26327  2sqreulem1  27427  2sqreunnlem1  27430  pntibndlem2  27572  elnnzs  28411  tgjustf  28559  iscgrglt  28600  islnoppd  28826  oppcom  28830  opphllem1  28833  opphllem5  28837  oppperpex  28839  hpgerlem  28851  colhp  28856  ax5seg  29025  uhgr2edg  29295  nbupgrres  29451  usgr2pthlem  29849  crctcshwlkn0lem5  29900  clwwlknonwwlknonb  30194  1pthond  30232  3pthdlem1  30252  frgrwopreglem5a  30399  grpoidinv  30597  nmcvcn  30784  leopmul  32223  resf1o  32822  trsp2cyc  33204  oddpwdc  34538  btwnconn1  36329  finminlem  36546  ptrecube  37987  poimirlem22  38009  isrngod  38265  paddasslem4  40315  cdleme21h  40826  cdleme26eALTN  40853  cdleme40m  40959  cdlemf2  41054  dicssdvh  41678  dihopelvalcpre  41740  dihmeetlem4preN  41798  dih1dimatlem0  41820  primrootscoprmpow  42584  primrootscoprbij  42587  aks6d1c5  42624  sticksstones22  42653  aks6d1c6lem3  42657  unitscyglem3  42682  unitscyglem5  42684  lzenom  43219  jm2.27c  43452  omltoe  43851  clrellem  44066  2pm13.193  44996  disjxp1  45517  dmrelrnrel  45671  infleinflem2  45815  mullimc  46061  mullimcf  46068  addlimc  46091  0ellimcdiv  46092  icccncfext  46330  stoweidlem52  46495  wallispilem4  46511  fourierdlem16  46566  fourierdlem21  46571  fourierdlem48  46597  fourierdlem51  46600  fourierdlem52  46601  fourierdlem54  46603  fourierdlem64  46613  fourierdlem76  46625  fourierdlem77  46626  fourierdlem80  46629  fourierdlem86  46635  fourierdlem87  46636  fourierdlem102  46651  fourierdlem114  46663  sge0f1o  46825  sge0split  46852  nnfoctbdjlem  46898  iundjiun  46903  ismeannd  46910  psmeasure  46914  isomennd  46974  hoidmvle  47043  ovncvr2  47054  dfatbrafv2b  47708  oexpnegnz  48169  clnbgrgrim  48425  usgrexmpl2trifr  48528  rngcinvALTV  48767  ringcinvALTV  48801  itsclc0b  49263  seposep  49416