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  6110  tpres  7130  f1oiso2  7281  poseq  8083  oewordri  8502  boxriin  8859  cantnfrescl  9561  cfsuc  10143  prsrlem1  10958  lemulge11  11979  lediv12a  12010  elnnz  12473  quoremz  13754  quoremnn0ALT  13756  fldiv  13759  modsumfzodifsn  13846  leexp1a  14077  faclbnd6  14201  wrdlen2i  14844  wwlktovfo  14860  setcinv  17992  sgrp2rid2  18829  grpidinv2  18905  eqg0subg  19103  gsumval3lem1  19812  rhmopp  20419  rngcinv  20547  ringcinv  20581  dvdsrzring  21393  cncnp2  23191  vitalilem1  25531  aaliou3lem2  26273  2sqreulem1  27379  2sqreunnlem1  27382  pntibndlem2  27524  elnnzs  28320  tgjustf  28446  iscgrglt  28487  islnoppd  28713  oppcom  28717  opphllem1  28720  opphllem5  28724  oppperpex  28726  hpgerlem  28738  colhp  28743  ax5seg  28911  uhgr2edg  29181  nbupgrres  29337  usgr2pthlem  29736  crctcshwlkn0lem5  29787  clwwlknonwwlknonb  30078  1pthond  30116  3pthdlem1  30136  frgrwopreglem5a  30283  grpoidinv  30480  nmcvcn  30667  leopmul  32106  resf1o  32705  trsp2cyc  33084  oddpwdc  34359  btwnconn1  36135  finminlem  36352  ptrecube  37660  poimirlem22  37682  isrngod  37938  paddasslem4  39862  cdleme21h  40373  cdleme26eALTN  40400  cdleme40m  40506  cdlemf2  40601  dicssdvh  41225  dihopelvalcpre  41287  dihmeetlem4preN  41345  dih1dimatlem0  41367  primrootscoprmpow  42132  primrootscoprbij  42135  aks6d1c5  42172  sticksstones22  42201  aks6d1c6lem3  42205  unitscyglem3  42230  unitscyglem5  42232  lzenom  42803  jm2.27c  43040  omltoe  43440  clrellem  43655  2pm13.193  44585  disjxp1  45106  dmrelrnrel  45263  infleinflem2  45409  mullimc  45656  mullimcf  45663  addlimc  45686  0ellimcdiv  45687  icccncfext  45925  stoweidlem52  46090  wallispilem4  46106  fourierdlem16  46161  fourierdlem21  46166  fourierdlem48  46192  fourierdlem51  46195  fourierdlem52  46196  fourierdlem54  46198  fourierdlem64  46208  fourierdlem76  46220  fourierdlem77  46221  fourierdlem80  46224  fourierdlem86  46230  fourierdlem87  46231  fourierdlem102  46246  fourierdlem114  46258  sge0f1o  46420  sge0split  46447  nnfoctbdjlem  46493  iundjiun  46498  ismeannd  46505  psmeasure  46509  isomennd  46569  hoidmvle  46638  ovncvr2  46649  dfatbrafv2b  47276  oexpnegnz  47709  clnbgrgrim  47965  usgrexmpl2trifr  48068  rngcinvALTV  48307  ringcinvALTV  48341  itsclc0b  48804  seposep  48957