Theorem jca31 518

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  3jca  1125  syl21anbrc  1341  xpdifid  5992  tpres  6940  f1oiso2  7084  oewordri  8201  boxriin  8487  cantnfrescl  9123  cfsuc  9668  prsrlem1  10483  lemulge11  11491  lediv12a  11522  elnnz  11979  quoremz  13218  quoremnn0ALT  13220  fldiv  13223  modsumfzodifsn  13307  leexp1a  13535  faclbnd6  13655  wrdlen2i  14295  wwlktovfo  14313  setcinv  17342  sgrp2rid2  18083  grpidinv2  18150  gsumval3lem1  19018  dvdsrzring  20176  cncnp2  21886  vitalilem1  24212  aaliou3lem2  24939  2sqreulem1  26030  2sqreunnlem1  26033  pntibndlem2  26175  tgjustf  26267  iscgrglt  26308  islnoppd  26534  oppcom  26538  opphllem1  26541  opphllem5  26545  oppperpex  26547  hpgerlem  26559  colhp  26564  ax5seg  26732  uhgr2edg  26998  nbupgrres  27154  usgr2pthlem  27552  crctcshwlkn0lem5  27600  clwwlknonwwlknonb  27891  1pthond  27929  3pthdlem1  27949  frgrwopreglem5a  28096  grpoidinv  28291  nmcvcn  28478  leopmul  29917  resf1o  30492  trsp2cyc  30815  rhmopp  30943  oddpwdc  31722  poseq  33208  btwnconn1  33675  finminlem  33779  ptrecube  35057  poimirlem22  35079  isrngod  35336  paddasslem4  37119  cdleme21h  37630  cdleme26eALTN  37657  cdleme40m  37763  cdlemf2  37858  dicssdvh  38482  dihopelvalcpre  38544  dihmeetlem4preN  38602  dih1dimatlem0  38624  metakunt17  39366  lzenom  39711  jm2.27c  39948  clrellem  40322  2pm13.193  41258  disjxp1  41703  dmrelrnrel  41856  infleinflem2  42003  mullimc  42258  mullimcf  42265  addlimc  42290  0ellimcdiv  42291  icccncfext  42529  stoweidlem52  42694  wallispilem4  42710  fourierdlem16  42765  fourierdlem21  42770  fourierdlem48  42796  fourierdlem51  42799  fourierdlem52  42800  fourierdlem54  42802  fourierdlem64  42812  fourierdlem76  42824  fourierdlem77  42825  fourierdlem80  42828  fourierdlem86  42834  fourierdlem87  42835  fourierdlem102  42850  fourierdlem114  42862  sge0f1o  43021  sge0split  43048  nnfoctbdjlem  43094  iundjiun  43099  ismeannd  43106  psmeasure  43110  isomennd  43170  hoidmvle  43239  ovncvr2  43250  dfatbrafv2b  43801  oexpnegnz  44196  rngcinv  44605  rngcinvALTV  44617  ringcinv  44656  ringcinvALTV  44680  itsclc0b  45186