Theorem jca31 504

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

Syntax hints:   → wi 4   ∧ wa 382

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 197  df-an 383

This theorem is referenced by:  3jca  1122  syl21anc  1475  xpdifid  5703  tpres  6610  f1oiso2  6745  oewordri  7826  boxriin  8104  cantnfrescl  8737  cfsuc  9281  genpcl  10032  ltexprlem5  10064  prsrlem1  10095  lemulge11  11087  lediv12a  11118  elnnz  11589  quoremz  12862  quoremnn0ALT  12864  fldiv  12867  modsumfzodifsn  12951  leexp1a  13126  faclbnd6  13290  wrdlen2i  13896  wwlktovfo  13911  setcinv  16947  sgrp2rid2  17621  grpidinv2  17682  mhmfmhm  17746  gsumval3lem1  18513  dvdsrzring  20046  scmatmhm  20558  cncnp2  21306  vitalilem1  23596  aaliou3lem2  24318  pntibndlem2  25501  iscgrglt  25630  islnoppd  25853  oppcom  25857  opphllem1  25860  opphllem5  25864  oppperpex  25866  hpgerlem  25878  colopp  25882  colhp  25883  ax5seg  26039  uhgr2edg  26322  nbupgrres  26488  usgr2pthlem  26894  crctcshwlkn0lem5  26942  wlknwwlksnsurOLD  27024  wlkwwlksurOLD  27032  clwwlknonwwlknonb  27281  clwwlknonwwlknonbOLD  27282  1pthond  27324  3pthdlem1  27344  frgrwopreglem5a  27493  grpoidinv  27702  nmcvcn  27890  leopmul  29333  resf1o  29845  rhmopp  30159  oddpwdc  30756  poseq  32090  btwnconn1  32545  finminlem  32649  bj-elid3  33424  ptrecube  33742  poimirlem22  33764  isrngod  34029  paddasslem4  35631  cdleme21h  36143  cdleme26eALTN  36170  cdleme40m  36276  cdlemf2  36371  dicssdvh  36996  dihopelvalcpre  37058  dihmeetlem4preN  37116  dih1dimatlem0  37138  lzenom  37859  jm2.27c  38100  clrellem  38455  2pm13.193  39293  disjxp1  39759  dmrelrnrel  39937  infleinflem2  40103  mullimc  40366  mullimcf  40373  addlimc  40398  0ellimcdiv  40399  cncfshift  40605  cncfperiod  40610  icccncfext  40618  stoweidlem52  40786  wallispilem4  40802  fourierdlem16  40857  fourierdlem21  40862  fourierdlem48  40888  fourierdlem51  40891  fourierdlem52  40892  fourierdlem54  40894  fourierdlem64  40904  fourierdlem76  40916  fourierdlem77  40917  fourierdlem80  40920  fourierdlem86  40926  fourierdlem87  40927  fourierdlem102  40942  fourierdlem114  40954  sge0f1o  41116  sge0split  41143  ismea  41185  nnfoctbdjlem  41189  iundjiun  41194  ismeannd  41201  psmeasure  41205  isomennd  41265  hoidmvle  41334  ovncvr2  41345  oexpnegnz  42117  rngcinv  42509  rngcinvALTV  42521  ringcinv  42560  ringcinvALTV  42584