Theorem jca31 515

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  3jca  1128  syl21anbrc  1344  xpdifid  6164  tpres  7198  f1oiso2  7345  poseq  8140  oewordri  8588  boxriin  8930  cantnfrescl  9667  cfsuc  10248  prsrlem1  11063  lemulge11  12072  lediv12a  12103  elnnz  12564  quoremz  13816  quoremnn0ALT  13818  fldiv  13821  modsumfzodifsn  13905  leexp1a  14136  faclbnd6  14255  wrdlen2i  14889  wwlktovfo  14905  setcinv  18036  sgrp2rid2  18803  grpidinv2  18878  eqg0subg  19067  gsumval3lem1  19767  rhmopp  20280  dvdsrzring  21022  cncnp2  22776  vitalilem1  25116  aaliou3lem2  25847  2sqreulem1  26938  2sqreunnlem1  26941  pntibndlem2  27083  tgjustf  27713  iscgrglt  27754  islnoppd  27980  oppcom  27984  opphllem1  27987  opphllem5  27991  oppperpex  27993  hpgerlem  28005  colhp  28010  ax5seg  28185  uhgr2edg  28454  nbupgrres  28610  usgr2pthlem  29009  crctcshwlkn0lem5  29057  clwwlknonwwlknonb  29348  1pthond  29386  3pthdlem1  29406  frgrwopreglem5a  29553  grpoidinv  29748  nmcvcn  29935  leopmul  31374  resf1o  31942  trsp2cyc  32269  oddpwdc  33341  btwnconn1  35061  finminlem  35191  ptrecube  36476  poimirlem22  36498  isrngod  36754  paddasslem4  38682  cdleme21h  39193  cdleme26eALTN  39220  cdleme40m  39326  cdlemf2  39421  dicssdvh  40045  dihopelvalcpre  40107  dihmeetlem4preN  40165  dih1dimatlem0  40187  sticksstones22  40972  metakunt17  40989  lzenom  41493  jm2.27c  41731  omltoe  42143  clrellem  42358  2pm13.193  43298  disjxp1  43741  dmrelrnrel  43910  infleinflem2  44067  mullimc  44318  mullimcf  44325  addlimc  44350  0ellimcdiv  44351  icccncfext  44589  stoweidlem52  44754  wallispilem4  44770  fourierdlem16  44825  fourierdlem21  44830  fourierdlem48  44856  fourierdlem51  44859  fourierdlem52  44860  fourierdlem54  44862  fourierdlem64  44872  fourierdlem76  44884  fourierdlem77  44885  fourierdlem80  44888  fourierdlem86  44894  fourierdlem87  44895  fourierdlem102  44910  fourierdlem114  44922  sge0f1o  45084  sge0split  45111  nnfoctbdjlem  45157  iundjiun  45162  ismeannd  45169  psmeasure  45173  isomennd  45233  hoidmvle  45302  ovncvr2  45313  dfatbrafv2b  45939  oexpnegnz  46332  rngcinv  46832  rngcinvALTV  46844  ringcinv  46883  ringcinvALTV  46907  itsclc0b  47411  seposep  47511