Theorem jca31 522

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  3jca  1140  syl21anbrc  1357  xpdifid  6149  tpres  7180  f1oiso2  7331  poseq  8132  oewordri  8556  boxriin  8916  cantnfrescl  9625  cfsuc  10208  prsrlem1  11024  lemulge11  12048  lediv12a  12079  elnnz  12572  quoremz  13859  quoremnn0ALT  13861  fldiv  13864  modsumfzodifsn  13951  leexp1a  14182  faclbnd6  14306  wrdlen2i  14949  wwlktovfo  14965  setcinv  18114  sgrp2rid2  18954  grpidinv2  19030  eqg0subg  19228  gsumval3lem1  19936  rhmopp  20546  rngcinv  20674  ringcinv  20708  dvdsrzring  21501  cncnp2  23329  vitalilem1  25658  aaliou3lem2  26395  2sqreulem1  27498  2sqreunnlem1  27501  pntibndlem2  27643  elnnzs  28482  tgjustf  28630  iscgrglt  28671  islnoppd  28897  oppcom  28901  opphllem1  28904  opphllem5  28908  oppperpex  28910  hpgerlem  28922  colhp  28927  ax5seg  29096  uhgr2edg  29366  nbupgrres  29522  usgr2pthlem  29920  crctcshwlkn0lem5  29971  clwwlknonwwlknonb  30265  1pthond  30303  3pthdlem1  30323  frgrwopreglem5a  30470  grpoidinv  30668  nmcvcn  30855  leopmul  32294  resf1o  32893  trsp2cyc  33264  oddpwdc  34612  btwnconn1  36412  finminlem  36639  ptrecube  38080  poimirlem22  38102  isrngod  38358  paddasslem4  40408  cdleme21h  40919  cdleme26eALTN  40946  cdleme40m  41052  cdlemf2  41147  dicssdvh  41771  dihopelvalcpre  41833  dihmeetlem4preN  41891  dih1dimatlem0  41913  primrootscoprmpow  42677  primrootscoprbij  42680  aks6d1c5  42717  sticksstones22  42746  aks6d1c6lem3  42750  unitscyglem3  42775  unitscyglem5  42777  lzenom  43312  jm2.27c  43545  omltoe  43944  clrellem  44159  2pm13.193  45089  disjxp1  45610  dmrelrnrel  45763  infleinflem2  45907  mullimc  46153  mullimcf  46160  addlimc  46183  0ellimcdiv  46184  icccncfext  46422  stoweidlem52  46587  wallispilem4  46603  fourierdlem16  46658  fourierdlem21  46663  fourierdlem48  46689  fourierdlem51  46692  fourierdlem52  46693  fourierdlem54  46695  fourierdlem64  46705  fourierdlem76  46717  fourierdlem77  46718  fourierdlem80  46721  fourierdlem86  46727  fourierdlem87  46728  fourierdlem102  46743  fourierdlem114  46755  sge0f1o  46917  sge0split  46944  nnfoctbdjlem  46990  iundjiun  46995  ismeannd  47002  psmeasure  47006  isomennd  47066  hoidmvle  47135  ovncvr2  47146  dfatbrafv2b  47800  oexpnegnz  48261  clnbgrgrim  48517  usgrexmpl2trifr  48620  rngcinvALTV  48859  ringcinvALTV  48893  itsclc0b  49355  seposep  49508