Theorem jca31 557

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  3jca  1242  syl21anc  1325  xpdifid  5562  tpres  6466  f1oiso2  6602  oewordri  7672  boxriin  7950  cantnfrescl  8573  cfsuc  9079  genpcl  9830  ltexprlem5  9862  prsrlem1  9893  lemulge11  10885  lediv12a  10916  elnnz  11387  quoremz  12654  quoremnn0ALT  12656  fldiv  12659  modsumfzodifsn  12743  leexp1a  12919  faclbnd6  13086  wrdlen2i  13686  wwlktovfo  13701  setcinv  16740  sgrp2rid2  17413  grpidinv2  17474  mhmfmhm  17538  gsumval3lem1  18306  dvdsrzring  19831  scmatmhm  20340  cncnp2  21085  vitalilem1  23376  vitalilem1OLD  23377  aaliou3lem2  24098  pntibndlem2  25280  iscgrglt  25409  islnoppd  25632  oppcom  25636  opphllem1  25639  opphllem5  25643  oppperpex  25645  hpgerlem  25657  colopp  25661  colhp  25662  ax5seg  25818  uhgr2edg  26100  nbupgrres  26266  usgr2pthlem  26659  crctcshwlkn0lem5  26706  wlknwwlksnsur  26776  wlkwwlksur  26783  1pthond  27004  3pthdlem1  27024  frgrwopreglem5a  27175  grpoidinv  27362  nmcvcn  27550  leopmul  28993  resf1o  29505  rhmopp  29819  oddpwdc  30416  poseq  31750  btwnconn1  32208  finminlem  32312  bj-elid3  33087  ptrecube  33409  poimirlem22  33431  isrngod  33697  paddasslem4  35109  cdleme21h  35622  cdleme26eALTN  35649  cdleme40m  35755  cdlemf2  35850  dicssdvh  36475  dihopelvalcpre  36537  dihmeetlem4preN  36595  dih1dimatlem0  36617  lzenom  37333  jm2.27c  37574  clrellem  37929  2pm13.193  38768  disjxp1  39238  dmrelrnrel  39419  infleinflem2  39587  mullimc  39848  mullimcf  39855  addlimc  39880  0ellimcdiv  39881  cncfshift  40087  cncfperiod  40092  icccncfext  40100  stoweidlem52  40269  wallispilem4  40285  fourierdlem16  40340  fourierdlem21  40345  fourierdlem48  40371  fourierdlem51  40374  fourierdlem52  40375  fourierdlem54  40377  fourierdlem64  40387  fourierdlem76  40399  fourierdlem77  40400  fourierdlem80  40403  fourierdlem86  40409  fourierdlem87  40410  fourierdlem102  40425  fourierdlem114  40437  sge0f1o  40599  sge0split  40626  ismea  40668  nnfoctbdjlem  40672  iundjiun  40677  ismeannd  40684  psmeasure  40688  isomennd  40745  hoidmvle  40814  ovncvr2  40825  oexpnegnz  41589  rngcinv  41981  rngcinvALTV  41993  ringcinv  42032  ringcinvALTV  42056