Theorem jca31 523

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  3jca  1144  syl21anbrc  1361  xpdifid  6164  xpdifcnvepel  6165  tpres  7197  f1oiso2  7348  poseq  8150  oewordri  8574  boxriin  8934  cantnfrescl  9641  cfsuc  10237  prsrlem1  11053  lemulge11  12073  lediv12a  12104  elnnz  12597  quoremz  13884  quoremnn0ALT  13886  fldiv  13889  modsumfzodifsn  13976  leexp1a  14207  faclbnd6  14331  wrdlen2i  14975  wwlktovfo  14991  setcinv  18143  sgrp2rid2  18984  grpidinv2  19060  eqg0subg  19263  gsumval3lem1  19971  rhmopp  20588  rngcinv  20718  ringcinv  20752  dvdsrzring  21576  cncnp2  23403  vitalilem1  25732  aaliou3lem2  26469  2sqreulem1  27572  2sqreunnlem1  27575  pntibndlem2  27717  elnnzs  28556  tgjustf  28704  iscgrglt  28745  islnoppd  28976  oppcom  28980  opphllem1  28983  opphllem5  28987  oppperpex  28989  hpgerlem  29002  colhp  29007  prlngsym  29142  ax5seg  29225  uhgr2edg  29495  nbupgrres  29651  usgr2pthlem  30049  crctcshwlkn0lem5  30100  clwwlknonwwlknonb  30394  1pthond  30432  3pthdlem1  30452  frgrwopreglem5a  30599  grpoidinv  30797  nmcvcn  30984  leopmul  32423  resf1o  33012  trsp2cyc  33380  oddpwdc  34685  btwnconn1  36488  finminlem  36714  ptrecube  38154  poimirlem22  38176  isrngod  38432  paddasslem4  40482  cdleme21h  40993  cdleme26eALTN  41020  cdleme40m  41126  cdlemf2  41221  dicssdvh  41845  dihopelvalcpre  41907  dihmeetlem4preN  41965  dih1dimatlem0  41987  primrootscoprmpow  42751  primrootscoprbij  42754  aks6d1c5  42791  sticksstones22  42820  aks6d1c6lem3  42824  unitscyglem3  42849  unitscyglem5  42851  lzenom  43386  jm2.27c  43619  omltoe  44018  clrellem  44233  2pm13.193  45146  disjxp1  45674  dmrelrnrel  45827  infleinflem2  45971  mullimc  46217  mullimcf  46224  addlimc  46247  0ellimcdiv  46248  icccncfext  46486  stoweidlem52  46651  wallispilem4  46667  fourierdlem16  46722  fourierdlem21  46727  fourierdlem48  46753  fourierdlem51  46756  fourierdlem52  46757  fourierdlem54  46759  fourierdlem64  46769  fourierdlem76  46781  fourierdlem77  46782  fourierdlem80  46785  fourierdlem86  46791  fourierdlem87  46792  fourierdlem102  46807  fourierdlem114  46819  sge0f1o  46981  sge0split  47008  nnfoctbdjlem  47054  iundjiun  47059  ismeannd  47066  psmeasure  47070  isomennd  47130  hoidmvle  47199  ovncvr2  47210  dfatbrafv2b  47864  oexpnegnz  48325  clnbgrgrim  48581  usgrexmpl2trifr  48684  rngcinvALTV  48923  ringcinvALTV  48957  itsclc0b  49430  seposep  49582