Theorem jca31 514

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  3jca  1128  syl21anbrc  1345  xpdifid  6123  tpres  7144  f1oiso2  7295  poseq  8097  oewordri  8516  boxriin  8874  cantnfrescl  9577  cfsuc  10159  prsrlem1  10974  lemulge11  11995  lediv12a  12026  elnnz  12489  quoremz  13766  quoremnn0ALT  13768  fldiv  13771  modsumfzodifsn  13858  leexp1a  14089  faclbnd6  14213  wrdlen2i  14856  wwlktovfo  14872  setcinv  18005  sgrp2rid2  18842  grpidinv2  18918  eqg0subg  19116  gsumval3lem1  19825  rhmopp  20433  rngcinv  20561  ringcinv  20595  dvdsrzring  21407  cncnp2  23216  vitalilem1  25556  aaliou3lem2  26298  2sqreulem1  27404  2sqreunnlem1  27407  pntibndlem2  27549  elnnzs  28345  tgjustf  28471  iscgrglt  28512  islnoppd  28738  oppcom  28742  opphllem1  28745  opphllem5  28749  oppperpex  28751  hpgerlem  28763  colhp  28768  ax5seg  28937  uhgr2edg  29207  nbupgrres  29363  usgr2pthlem  29762  crctcshwlkn0lem5  29813  clwwlknonwwlknonb  30107  1pthond  30145  3pthdlem1  30165  frgrwopreglem5a  30312  grpoidinv  30509  nmcvcn  30696  leopmul  32135  resf1o  32737  trsp2cyc  33133  oddpwdc  34439  btwnconn1  36217  finminlem  36434  ptrecube  37733  poimirlem22  37755  isrngod  38011  paddasslem4  39995  cdleme21h  40506  cdleme26eALTN  40533  cdleme40m  40639  cdlemf2  40734  dicssdvh  41358  dihopelvalcpre  41420  dihmeetlem4preN  41478  dih1dimatlem0  41500  primrootscoprmpow  42265  primrootscoprbij  42268  aks6d1c5  42305  sticksstones22  42334  aks6d1c6lem3  42338  unitscyglem3  42363  unitscyglem5  42365  lzenom  42927  jm2.27c  43164  omltoe  43564  clrellem  43779  2pm13.193  44709  disjxp1  45230  dmrelrnrel  45386  infleinflem2  45531  mullimc  45778  mullimcf  45785  addlimc  45808  0ellimcdiv  45809  icccncfext  46047  stoweidlem52  46212  wallispilem4  46228  fourierdlem16  46283  fourierdlem21  46288  fourierdlem48  46314  fourierdlem51  46317  fourierdlem52  46318  fourierdlem54  46320  fourierdlem64  46330  fourierdlem76  46342  fourierdlem77  46343  fourierdlem80  46346  fourierdlem86  46352  fourierdlem87  46353  fourierdlem102  46368  fourierdlem114  46380  sge0f1o  46542  sge0split  46569  nnfoctbdjlem  46615  iundjiun  46620  ismeannd  46627  psmeasure  46631  isomennd  46691  hoidmvle  46760  ovncvr2  46771  dfatbrafv2b  47407  oexpnegnz  47840  clnbgrgrim  48096  usgrexmpl2trifr  48199  rngcinvALTV  48438  ringcinvALTV  48472  itsclc0b  48934  seposep  49087