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  1129  syl21anbrc  1346  xpdifid  6126  tpres  7149  f1oiso2  7300  poseq  8101  oewordri  8521  boxriin  8881  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  20477  rngcinv  20605  ringcinv  20639  dvdsrzring  21451  cncnp2  23256  vitalilem1  25585  aaliou3lem2  26320  2sqreulem1  27423  2sqreunnlem1  27426  pntibndlem2  27568  elnnzs  28407  tgjustf  28555  iscgrglt  28596  islnoppd  28822  oppcom  28826  opphllem1  28829  opphllem5  28833  oppperpex  28835  hpgerlem  28847  colhp  28852  ax5seg  29021  uhgr2edg  29291  nbupgrres  29447  usgr2pthlem  29846  crctcshwlkn0lem5  29897  clwwlknonwwlknonb  30191  1pthond  30229  3pthdlem1  30249  frgrwopreglem5a  30396  grpoidinv  30594  nmcvcn  30781  leopmul  32220  resf1o  32818  trsp2cyc  33199  oddpwdc  34514  btwnconn1  36299  finminlem  36516  ptrecube  37955  poimirlem22  37977  isrngod  38233  paddasslem4  40283  cdleme21h  40794  cdleme26eALTN  40821  cdleme40m  40927  cdlemf2  41022  dicssdvh  41646  dihopelvalcpre  41708  dihmeetlem4preN  41766  dih1dimatlem0  41788  primrootscoprmpow  42552  primrootscoprbij  42555  aks6d1c5  42592  sticksstones22  42621  aks6d1c6lem3  42625  unitscyglem3  42650  unitscyglem5  42652  lzenom  43216  jm2.27c  43453  omltoe  43852  clrellem  44067  2pm13.193  44997  disjxp1  45518  dmrelrnrel  45673  infleinflem2  45818  mullimc  46064  mullimcf  46071  addlimc  46094  0ellimcdiv  46095  icccncfext  46333  stoweidlem52  46498  wallispilem4  46514  fourierdlem16  46569  fourierdlem21  46574  fourierdlem48  46600  fourierdlem51  46603  fourierdlem52  46604  fourierdlem54  46606  fourierdlem64  46616  fourierdlem76  46628  fourierdlem77  46629  fourierdlem80  46632  fourierdlem86  46638  fourierdlem87  46639  fourierdlem102  46654  fourierdlem114  46666  sge0f1o  46828  sge0split  46855  nnfoctbdjlem  46901  iundjiun  46906  ismeannd  46913  psmeasure  46917  isomennd  46977  hoidmvle  47046  ovncvr2  47057  dfatbrafv2b  47705  oexpnegnz  48166  clnbgrgrim  48422  usgrexmpl2trifr  48525  rngcinvALTV  48764  ringcinvALTV  48798  itsclc0b  49260  seposep  49413