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  1344  xpdifid  6199  tpres  7238  f1oiso2  7388  poseq  8199  oewordri  8648  boxriin  8998  cantnfrescl  9745  cfsuc  10326  prsrlem1  11141  lemulge11  12157  lediv12a  12188  elnnz  12649  quoremz  13906  quoremnn0ALT  13908  fldiv  13911  modsumfzodifsn  13995  leexp1a  14225  faclbnd6  14348  wrdlen2i  14991  wwlktovfo  15007  setcinv  18157  sgrp2rid2  18961  grpidinv2  19037  eqg0subg  19236  gsumval3lem1  19947  rhmopp  20535  rngcinv  20659  ringcinv  20693  dvdsrzring  21495  cncnp2  23310  vitalilem1  25662  aaliou3lem2  26403  2sqreulem1  27508  2sqreunnlem1  27511  pntibndlem2  27653  elnnzs  28405  tgjustf  28499  iscgrglt  28540  islnoppd  28766  oppcom  28770  opphllem1  28773  opphllem5  28777  oppperpex  28779  hpgerlem  28791  colhp  28796  ax5seg  28971  uhgr2edg  29243  nbupgrres  29399  usgr2pthlem  29799  crctcshwlkn0lem5  29847  clwwlknonwwlknonb  30138  1pthond  30176  3pthdlem1  30196  frgrwopreglem5a  30343  grpoidinv  30540  nmcvcn  30727  leopmul  32166  resf1o  32744  trsp2cyc  33116  oddpwdc  34319  btwnconn1  36065  finminlem  36284  ptrecube  37580  poimirlem22  37602  isrngod  37858  paddasslem4  39780  cdleme21h  40291  cdleme26eALTN  40318  cdleme40m  40424  cdlemf2  40519  dicssdvh  41143  dihopelvalcpre  41205  dihmeetlem4preN  41263  dih1dimatlem0  41285  primrootscoprmpow  42056  primrootscoprbij  42059  aks6d1c5  42096  sticksstones22  42125  aks6d1c6lem3  42129  unitscyglem3  42154  unitscyglem5  42156  metakunt17  42178  lzenom  42726  jm2.27c  42964  omltoe  43369  clrellem  43584  2pm13.193  44523  disjxp1  44971  dmrelrnrel  45133  infleinflem2  45286  mullimc  45537  mullimcf  45544  addlimc  45569  0ellimcdiv  45570  icccncfext  45808  stoweidlem52  45973  wallispilem4  45989  fourierdlem16  46044  fourierdlem21  46049  fourierdlem48  46075  fourierdlem51  46078  fourierdlem52  46079  fourierdlem54  46081  fourierdlem64  46091  fourierdlem76  46103  fourierdlem77  46104  fourierdlem80  46107  fourierdlem86  46113  fourierdlem87  46114  fourierdlem102  46129  fourierdlem114  46141  sge0f1o  46303  sge0split  46330  nnfoctbdjlem  46376  iundjiun  46381  ismeannd  46388  psmeasure  46392  isomennd  46452  hoidmvle  46521  ovncvr2  46532  dfatbrafv2b  47160  oexpnegnz  47552  clnbgrgrim  47786  usgrexmpl2trifr  47852  rngcinvALTV  47999  ringcinvALTV  48033  itsclc0b  48506  seposep  48605