Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  jca31 Structured version   Visualization version   GIF version

Theorem jca31 515
 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
StepHypRef Expression
1 jca31.1 . . 3 (𝜑𝜓)
2 jca31.2 . . 3 (𝜑𝜒)
31, 2jca 512 . 2 (𝜑 → (𝜓𝜒))
4 jca31.3 . 2 (𝜑𝜃)
53, 4jca 512 1 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396 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 208  df-an 397 This theorem is referenced by:  3jca  1122  syl21anbrc  1338  xpdifid  6022  tpres  6962  f1oiso2  7100  oewordri  8211  boxriin  8496  cantnfrescl  9131  cfsuc  9671  prsrlem1  10486  lemulge11  11494  lediv12a  11525  elnnz  11983  quoremz  13216  quoremnn0ALT  13218  fldiv  13221  modsumfzodifsn  13305  leexp1a  13532  faclbnd6  13652  wrdlen2i  14297  wwlktovfo  14315  setcinv  17343  sgrp2rid2  18027  grpidinv2  18091  gsumval3lem1  18948  dvdsrzring  20549  cncnp2  21808  vitalilem1  24127  aaliou3lem2  24850  2sqreulem1  25939  2sqreunnlem1  25942  pntibndlem2  26084  tgjustf  26176  iscgrglt  26217  islnoppd  26443  oppcom  26447  opphllem1  26450  opphllem5  26454  oppperpex  26456  hpgerlem  26468  colhp  26473  ax5seg  26641  uhgr2edg  26907  nbupgrres  27063  usgr2pthlem  27461  crctcshwlkn0lem5  27509  clwwlknonwwlknonb  27802  1pthond  27840  3pthdlem1  27860  frgrwopreglem5a  28007  grpoidinv  28202  nmcvcn  28389  leopmul  29828  resf1o  30382  trsp2cyc  30682  rhmopp  30809  oddpwdc  31501  poseq  32982  btwnconn1  33449  finminlem  33553  ptrecube  34762  poimirlem22  34784  isrngod  35047  paddasslem4  36829  cdleme21h  37340  cdleme26eALTN  37367  cdleme40m  37473  cdlemf2  37568  dicssdvh  38192  dihopelvalcpre  38254  dihmeetlem4preN  38312  dih1dimatlem0  38334  lzenom  39235  jm2.27c  39472  clrellem  39850  2pm13.193  40754  disjxp1  41199  dmrelrnrel  41358  infleinflem2  41507  mullimc  41765  mullimcf  41772  addlimc  41797  0ellimcdiv  41798  icccncfext  42038  stoweidlem52  42206  wallispilem4  42222  fourierdlem16  42277  fourierdlem21  42282  fourierdlem48  42308  fourierdlem51  42311  fourierdlem52  42312  fourierdlem54  42314  fourierdlem64  42324  fourierdlem76  42336  fourierdlem77  42337  fourierdlem80  42340  fourierdlem86  42346  fourierdlem87  42347  fourierdlem102  42362  fourierdlem114  42374  sge0f1o  42533  sge0split  42560  nnfoctbdjlem  42606  iundjiun  42611  ismeannd  42618  psmeasure  42622  isomennd  42682  hoidmvle  42751  ovncvr2  42762  dfatbrafv2b  43313  oexpnegnz  43678  rngcinv  44087  rngcinvALTV  44099  ringcinv  44138  ringcinvALTV  44162  itsclc0b  44594
 Copyright terms: Public domain W3C validator