Theorem jca31 516

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  3jca  1129  syl21anbrc  1345  xpdifid  6168  tpres  7202  f1oiso2  7349  poseq  8144  oewordri  8592  boxriin  8934  cantnfrescl  9671  cfsuc  10252  prsrlem1  11067  lemulge11  12076  lediv12a  12107  elnnz  12568  quoremz  13820  quoremnn0ALT  13822  fldiv  13825  modsumfzodifsn  13909  leexp1a  14140  faclbnd6  14259  wrdlen2i  14893  wwlktovfo  14909  setcinv  18040  sgrp2rid2  18807  grpidinv2  18882  eqg0subg  19073  gsumval3lem1  19773  rhmopp  20288  dvdsrzring  21031  cncnp2  22785  vitalilem1  25125  aaliou3lem2  25856  2sqreulem1  26949  2sqreunnlem1  26952  pntibndlem2  27094  tgjustf  27724  iscgrglt  27765  islnoppd  27991  oppcom  27995  opphllem1  27998  opphllem5  28002  oppperpex  28004  hpgerlem  28016  colhp  28021  ax5seg  28196  uhgr2edg  28465  nbupgrres  28621  usgr2pthlem  29020  crctcshwlkn0lem5  29068  clwwlknonwwlknonb  29359  1pthond  29397  3pthdlem1  29417  frgrwopreglem5a  29564  grpoidinv  29761  nmcvcn  29948  leopmul  31387  resf1o  31955  trsp2cyc  32282  oddpwdc  33353  btwnconn1  35073  finminlem  35203  ptrecube  36488  poimirlem22  36510  isrngod  36766  paddasslem4  38694  cdleme21h  39205  cdleme26eALTN  39232  cdleme40m  39338  cdlemf2  39433  dicssdvh  40057  dihopelvalcpre  40119  dihmeetlem4preN  40177  dih1dimatlem0  40199  sticksstones22  40984  metakunt17  41001  lzenom  41508  jm2.27c  41746  omltoe  42158  clrellem  42373  2pm13.193  43313  disjxp1  43756  dmrelrnrel  43925  infleinflem2  44081  mullimc  44332  mullimcf  44339  addlimc  44364  0ellimcdiv  44365  icccncfext  44603  stoweidlem52  44768  wallispilem4  44784  fourierdlem16  44839  fourierdlem21  44844  fourierdlem48  44870  fourierdlem51  44873  fourierdlem52  44874  fourierdlem54  44876  fourierdlem64  44886  fourierdlem76  44898  fourierdlem77  44899  fourierdlem80  44902  fourierdlem86  44908  fourierdlem87  44909  fourierdlem102  44924  fourierdlem114  44936  sge0f1o  45098  sge0split  45125  nnfoctbdjlem  45171  iundjiun  45176  ismeannd  45183  psmeasure  45187  isomennd  45247  hoidmvle  45316  ovncvr2  45327  dfatbrafv2b  45953  oexpnegnz  46346  rngcinv  46879  rngcinvALTV  46891  ringcinv  46930  ringcinvALTV  46954  itsclc0b  47458  seposep  47558