Theorem jca31 555

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  3jca  1235  syl21anc  1317  xpdifid  5481  tpres  6371  f1oiso2  6502  oewordri  7559  boxriin  7836  cantnfrescl  8456  cfsuc  8962  genpcl  9709  ltexprlem5  9741  prsrlem1  9772  lemulge11  10764  lediv12a  10795  elnnz  11264  quoremz  12516  quoremnn0ALT  12518  fldiv  12521  modsumfzodifsn  12605  leexp1a  12781  faclbnd6  12948  wrdlen2i  13534  wwlktovfo  13549  setcinv  16563  sgrp2rid2  17236  grpidinv2  17297  mhmfmhm  17361  gsumval3lem1  18129  dvdsrzring  19650  scmatmhm  20159  cncnp2  20895  vitalilem1  23182  vitalilem1OLD  23183  aaliou3lem2  23902  pntibndlem2  25080  iscgrglt  25209  islnoppd  25432  oppcom  25436  opphllem1  25439  opphllem2  25440  opphllem5  25443  oppperpex  25445  hpgerlem  25457  colopp  25461  colhp  25462  ax5seg  25618  constr3lem4  26175  wlknwwlknsur  26240  wlkiswwlksur  26247  frgrancvvdeqlem4  26560  usg2spot2nb  26592  grpoidinv  26746  nmcvcn  26934  leopmul  28377  resf1o  28893  rhmopp  29150  oddpwdc  29743  poseq  30994  btwnconn1  31378  finminlem  31482  bj-elid3  32264  ptrecube  32579  poimirlem22  32601  isrngod  32867  paddasslem4  34127  cdleme21h  34640  cdleme26eALTN  34667  cdleme40m  34773  cdlemf2  34868  dicssdvh  35493  dihopelvalcpre  35555  dihmeetlem4preN  35613  dih1dimatlem0  35635  lzenom  36351  jm2.27c  36592  clrellem  36948  2pm13.193  37789  disjxp1  38263  dmrelrnrel  38414  infleinflem2  38528  mullimc  38683  mullimcf  38690  addlimc  38715  0ellimcdiv  38716  cncfshift  38759  cncfperiod  38764  icccncfext  38773  stoweidlem52  38945  wallispilem4  38961  fourierdlem16  39016  fourierdlem21  39021  fourierdlem48  39047  fourierdlem51  39050  fourierdlem52  39051  fourierdlem54  39053  fourierdlem64  39063  fourierdlem76  39075  fourierdlem77  39076  fourierdlem80  39079  fourierdlem86  39085  fourierdlem87  39086  fourierdlem102  39101  fourierdlem114  39113  sge0f1o  39275  sge0split  39302  ismea  39344  nnfoctbdjlem  39348  iundjiun  39353  ismeannd  39360  psmeasure  39364  isomennd  39421  hoidmvle  39490  ovncvr2  39501  oexpnegnz  40127  uhgr2edg  40435  nbupgrres  40592  usgr2pthlem  40969  crctcsh1wlkn0lem5  41017  wlknwwlksnsur  41087  wlkwwlksur  41094  1pthond  41311  3pthdlem1  41331  frgrncvvdeqlem4  41472  fusgr2wsp2nb  41498  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  ringcinvALTV  41848