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  6126  tpres  7147  f1oiso2  7298  poseq  8100  oewordri  8520  boxriin  8878  cantnfrescl  9585  cfsuc  10167  prsrlem1  10983  lemulge11  12004  lediv12a  12035  elnnz  12498  quoremz  13775  quoremnn0ALT  13777  fldiv  13780  modsumfzodifsn  13867  leexp1a  14098  faclbnd6  14222  wrdlen2i  14865  wwlktovfo  14881  setcinv  18014  sgrp2rid2  18851  grpidinv2  18927  eqg0subg  19125  gsumval3lem1  19834  rhmopp  20442  rngcinv  20570  ringcinv  20604  dvdsrzring  21416  cncnp2  23225  vitalilem1  25565  aaliou3lem2  26307  2sqreulem1  27413  2sqreunnlem1  27416  pntibndlem2  27558  elnnzs  28397  tgjustf  28545  iscgrglt  28586  islnoppd  28812  oppcom  28816  opphllem1  28819  opphllem5  28823  oppperpex  28825  hpgerlem  28837  colhp  28842  ax5seg  29011  uhgr2edg  29281  nbupgrres  29437  usgr2pthlem  29836  crctcshwlkn0lem5  29887  clwwlknonwwlknonb  30181  1pthond  30219  3pthdlem1  30239  frgrwopreglem5a  30386  grpoidinv  30583  nmcvcn  30770  leopmul  32209  resf1o  32809  trsp2cyc  33205  oddpwdc  34511  btwnconn1  36295  finminlem  36512  ptrecube  37821  poimirlem22  37843  isrngod  38099  paddasslem4  40083  cdleme21h  40594  cdleme26eALTN  40621  cdleme40m  40727  cdlemf2  40822  dicssdvh  41446  dihopelvalcpre  41508  dihmeetlem4preN  41566  dih1dimatlem0  41588  primrootscoprmpow  42353  primrootscoprbij  42356  aks6d1c5  42393  sticksstones22  42422  aks6d1c6lem3  42426  unitscyglem3  42451  unitscyglem5  42453  lzenom  43012  jm2.27c  43249  omltoe  43648  clrellem  43863  2pm13.193  44793  disjxp1  45314  dmrelrnrel  45470  infleinflem2  45615  mullimc  45862  mullimcf  45869  addlimc  45892  0ellimcdiv  45893  icccncfext  46131  stoweidlem52  46296  wallispilem4  46312  fourierdlem16  46367  fourierdlem21  46372  fourierdlem48  46398  fourierdlem51  46401  fourierdlem52  46402  fourierdlem54  46404  fourierdlem64  46414  fourierdlem76  46426  fourierdlem77  46427  fourierdlem80  46430  fourierdlem86  46436  fourierdlem87  46437  fourierdlem102  46452  fourierdlem114  46464  sge0f1o  46626  sge0split  46653  nnfoctbdjlem  46699  iundjiun  46704  ismeannd  46711  psmeasure  46715  isomennd  46775  hoidmvle  46844  ovncvr2  46855  dfatbrafv2b  47491  oexpnegnz  47924  clnbgrgrim  48180  usgrexmpl2trifr  48283  rngcinvALTV  48522  ringcinvALTV  48556  itsclc0b  49018  seposep  49171