Theorem jca31 524

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  3jca  1146  syl21anbrc  1363  xpdifid  6159  xpdifcnvepel  6160  tpres  7205  f1oiso2  7358  poseq  8168  oewordri  8594  boxriin  8961  cantnfrescl  9670  cfsuc  10328  prsrlem1  11150  lemulge11  12172  lediv12a  12203  elnnz  12696  quoremz  13988  quoremnn0ALT  13990  fldiv  13993  modsumfzodifsn  14080  leexp1a  14311  faclbnd6  14436  wrdlen2i  15086  wwlktovfo  15104  setcinv  18258  sgrp2rid2  19118  grpidinv2  19201  eqg0subg  19404  gsumval3lem1  20112  rhmopp  20752  rngcinv  20882  ringcinv  20916  dvdsrzring  21760  cncnp2  23592  vitalilem1  25922  aaliou3lem2  26663  2sqreulem1  27766  2sqreunnlem1  27769  pntibndlem2  27911  elnnzs  28780  tgjustf  28928  iscgrglt  28970  islnoppd  29209  oppcom  29213  opphllem1  29216  opphllem5  29220  oppperpex  29222  hpgerlem  29236  colhp  29241  prlngsym  29412  ax5seg  29509  uhgr2edg  29782  nbupgrres  29938  usgr2pthlem  30342  crctcshwlkn0lem5  30396  clwwlknonwwlknonb  30690  1pthond  30728  3pthdlem1  30758  frgrwopreglem5a  30905  grpoidinv  31103  nmcvcn  31290  leopmul  32729  resf1o  33315  trsp2cyc  33677  oddpwdc  34979  btwnconn1  36846  finminlem  37086  ptrecube  38518  poimirlem22  38540  isrngod  38812  paddasslem4  40860  cdleme21h  41371  cdleme26eALTN  41398  cdleme40m  41504  cdlemf2  41599  dicssdvh  42223  dihopelvalcpre  42285  dihmeetlem4preN  42343  dih1dimatlem0  42365  primrootscoprmpow  43129  primrootscoprbij  43132  aks6d1c5  43169  sticksstones22  43198  aks6d1c6lem3  43202  unitscyglem3  43227  unitscyglem5  43229  lzenom  43760  jm2.27c  43993  omltoe  44392  clrellem  44607  2pm13.193  45520  disjxp1  46055  dmrelrnrel  46208  infleinflem2  46351  mullimc  46597  mullimcf  46604  addlimc  46627  0ellimcdiv  46628  icccncfext  46866  stoweidlem52  47031  wallispilem4  47047  fourierdlem16  47102  fourierdlem21  47107  fourierdlem48  47133  fourierdlem51  47136  fourierdlem52  47137  fourierdlem54  47139  fourierdlem64  47149  fourierdlem76  47161  fourierdlem77  47162  fourierdlem80  47165  fourierdlem86  47171  fourierdlem87  47172  fourierdlem102  47187  fourierdlem114  47199  sge0f1o  47361  sge0split  47388  nnfoctbdjlem  47434  iundjiun  47439  ismeannd  47446  psmeasure  47450  isomennd  47510  hoidmvle  47579  ovncvr2  47590  dfatbrafv2b  48284  oexpnegnz  48745  clnbgrgrim  49001  usgrexmpl2trifr  49104  rngcinvALTV  49342  ringcinvALTV  49376  itsclc0b  49853  seposep  50003