Theorem jca31 517

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  3jca  1124  syl21anbrc  1340  xpdifid  6020  tpres  6958  f1oiso2  7099  oewordri  8212  boxriin  8498  cantnfrescl  9133  cfsuc  9673  prsrlem1  10488  lemulge11  11496  lediv12a  11527  elnnz  11985  quoremz  13217  quoremnn0ALT  13219  fldiv  13222  modsumfzodifsn  13306  leexp1a  13533  faclbnd6  13653  wrdlen2i  14298  wwlktovfo  14316  setcinv  17344  sgrp2rid2  18085  grpidinv2  18152  gsumval3lem1  19019  dvdsrzring  20624  cncnp2  21883  vitalilem1  24203  aaliou3lem2  24926  2sqreulem1  26016  2sqreunnlem1  26019  pntibndlem2  26161  tgjustf  26253  iscgrglt  26294  islnoppd  26520  oppcom  26524  opphllem1  26527  opphllem5  26531  oppperpex  26533  hpgerlem  26545  colhp  26550  ax5seg  26718  uhgr2edg  26984  nbupgrres  27140  usgr2pthlem  27538  crctcshwlkn0lem5  27586  clwwlknonwwlknonb  27879  1pthond  27917  3pthdlem1  27937  frgrwopreglem5a  28084  grpoidinv  28279  nmcvcn  28466  leopmul  29905  resf1o  30460  trsp2cyc  30760  rhmopp  30887  oddpwdc  31607  poseq  33090  btwnconn1  33557  finminlem  33661  ptrecube  34886  poimirlem22  34908  isrngod  35170  paddasslem4  36953  cdleme21h  37464  cdleme26eALTN  37491  cdleme40m  37597  cdlemf2  37692  dicssdvh  38316  dihopelvalcpre  38378  dihmeetlem4preN  38436  dih1dimatlem0  38458  lzenom  39360  jm2.27c  39597  clrellem  39975  2pm13.193  40879  disjxp1  41324  dmrelrnrel  41482  infleinflem2  41631  mullimc  41889  mullimcf  41896  addlimc  41921  0ellimcdiv  41922  icccncfext  42162  stoweidlem52  42330  wallispilem4  42346  fourierdlem16  42401  fourierdlem21  42406  fourierdlem48  42432  fourierdlem51  42435  fourierdlem52  42436  fourierdlem54  42438  fourierdlem64  42448  fourierdlem76  42460  fourierdlem77  42461  fourierdlem80  42464  fourierdlem86  42470  fourierdlem87  42471  fourierdlem102  42486  fourierdlem114  42498  sge0f1o  42657  sge0split  42684  nnfoctbdjlem  42730  iundjiun  42735  ismeannd  42742  psmeasure  42746  isomennd  42806  hoidmvle  42875  ovncvr2  42886  dfatbrafv2b  43437  oexpnegnz  43836  rngcinv  44245  rngcinvALTV  44257  ringcinv  44296  ringcinvALTV  44320  itsclc0b  44752