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

This theorem is referenced by:  3jca  1126  syl21anbrc  1342  xpdifid  6068  tpres  7070  f1oiso2  7216  oewordri  8399  boxriin  8702  cantnfrescl  9395  cfsuc  9997  prsrlem1  10812  lemulge11  11820  lediv12a  11851  elnnz  12312  quoremz  13556  quoremnn0ALT  13558  fldiv  13561  modsumfzodifsn  13645  leexp1a  13874  faclbnd6  13994  wrdlen2i  14636  wwlktovfo  14654  setcinv  17786  sgrp2rid2  18546  grpidinv2  18615  gsumval3lem1  19487  dvdsrzring  20664  cncnp2  22413  vitalilem1  24753  aaliou3lem2  25484  2sqreulem1  26575  2sqreunnlem1  26578  pntibndlem2  26720  tgjustf  26815  iscgrglt  26856  islnoppd  27082  oppcom  27086  opphllem1  27089  opphllem5  27093  oppperpex  27095  hpgerlem  27107  colhp  27112  ax5seg  27287  uhgr2edg  27556  nbupgrres  27712  usgr2pthlem  28110  crctcshwlkn0lem5  28158  clwwlknonwwlknonb  28449  1pthond  28487  3pthdlem1  28507  frgrwopreglem5a  28654  grpoidinv  28849  nmcvcn  29036  leopmul  30475  resf1o  31044  trsp2cyc  31369  rhmopp  31497  oddpwdc  32300  poseq  33781  btwnconn1  34382  finminlem  34486  ptrecube  35756  poimirlem22  35778  isrngod  36035  paddasslem4  37816  cdleme21h  38327  cdleme26eALTN  38354  cdleme40m  38460  cdlemf2  38555  dicssdvh  39179  dihopelvalcpre  39241  dihmeetlem4preN  39299  dih1dimatlem0  39321  sticksstones22  40104  metakunt17  40121  lzenom  40572  jm2.27c  40809  clrellem  41183  2pm13.193  42125  disjxp1  42570  dmrelrnrel  42718  infleinflem2  42864  mullimc  43111  mullimcf  43118  addlimc  43143  0ellimcdiv  43144  icccncfext  43382  stoweidlem52  43547  wallispilem4  43563  fourierdlem16  43618  fourierdlem21  43623  fourierdlem48  43649  fourierdlem51  43652  fourierdlem52  43653  fourierdlem54  43655  fourierdlem64  43665  fourierdlem76  43677  fourierdlem77  43678  fourierdlem80  43681  fourierdlem86  43687  fourierdlem87  43688  fourierdlem102  43703  fourierdlem114  43715  sge0f1o  43874  sge0split  43901  nnfoctbdjlem  43947  iundjiun  43952  ismeannd  43959  psmeasure  43963  isomennd  44023  hoidmvle  44092  ovncvr2  44103  dfatbrafv2b  44688  oexpnegnz  45082  rngcinv  45491  rngcinvALTV  45503  ringcinv  45542  ringcinvALTV  45566  itsclc0b  46070  seposep  46171