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  1146  syl21anbrc  1363  xpdifid  6167  xpdifcnvepel  6168  tpres  7201  f1oiso2  7352  poseq  8155  oewordri  8579  boxriin  8939  cantnfrescl  9646  cfsuc  10242  prsrlem1  11058  lemulge11  12078  lediv12a  12109  elnnz  12602  quoremz  13890  quoremnn0ALT  13892  fldiv  13895  modsumfzodifsn  13982  leexp1a  14213  faclbnd6  14337  wrdlen2i  14981  wwlktovfo  14997  setcinv  18148  sgrp2rid2  18989  grpidinv2  19065  eqg0subg  19268  gsumval3lem1  19976  rhmopp  20593  rngcinv  20723  ringcinv  20757  dvdsrzring  21592  cncnp2  23419  vitalilem1  25748  aaliou3lem2  26487  2sqreulem1  27591  2sqreunnlem1  27594  pntibndlem2  27736  elnnzs  28575  tgjustf  28723  iscgrglt  28764  islnoppd  29002  oppcom  29006  opphllem1  29009  opphllem5  29013  oppperpex  29015  hpgerlem  29028  colhp  29033  prlngsym  29172  ax5seg  29269  uhgr2edg  29539  nbupgrres  29695  usgr2pthlem  30093  crctcshwlkn0lem5  30144  clwwlknonwwlknonb  30438  1pthond  30476  3pthdlem1  30496  frgrwopreglem5a  30643  grpoidinv  30841  nmcvcn  31028  leopmul  32467  resf1o  33056  trsp2cyc  33424  oddpwdc  34725  btwnconn1  36574  finminlem  36810  ptrecube  38252  poimirlem22  38274  isrngod  38530  paddasslem4  40578  cdleme21h  41089  cdleme26eALTN  41116  cdleme40m  41222  cdlemf2  41317  dicssdvh  41941  dihopelvalcpre  42003  dihmeetlem4preN  42061  dih1dimatlem0  42083  primrootscoprmpow  42847  primrootscoprbij  42850  aks6d1c5  42887  sticksstones22  42916  aks6d1c6lem3  42920  unitscyglem3  42945  unitscyglem5  42947  lzenom  43484  jm2.27c  43717  omltoe  44116  clrellem  44331  2pm13.193  45244  disjxp1  45772  dmrelrnrel  45925  infleinflem2  46069  mullimc  46315  mullimcf  46322  addlimc  46345  0ellimcdiv  46346  icccncfext  46584  stoweidlem52  46749  wallispilem4  46765  fourierdlem16  46820  fourierdlem21  46825  fourierdlem48  46851  fourierdlem51  46854  fourierdlem52  46855  fourierdlem54  46857  fourierdlem64  46867  fourierdlem76  46879  fourierdlem77  46880  fourierdlem80  46883  fourierdlem86  46889  fourierdlem87  46890  fourierdlem102  46905  fourierdlem114  46917  sge0f1o  47079  sge0split  47106  nnfoctbdjlem  47152  iundjiun  47157  ismeannd  47164  psmeasure  47168  isomennd  47228  hoidmvle  47297  ovncvr2  47308  dfatbrafv2b  47965  oexpnegnz  48426  clnbgrgrim  48682  usgrexmpl2trifr  48785  rngcinvALTV  49024  ringcinvALTV  49058  itsclc0b  49535  seposep  49687