MPE Home 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  1120  syl21anbrc  1336  xpdifid  6018  tpres  6955  f1oiso2  7094  oewordri  8207  boxriin  8492  cantnfrescl  9127  cfsuc  9667  prsrlem1  10482  lemulge11  11490  lediv12a  11521  elnnz  11979  quoremz  13211  quoremnn0ALT  13213  fldiv  13216  modsumfzodifsn  13300  leexp1a  13527  faclbnd6  13647  wrdlen2i  14292  wwlktovfo  14310  setcinv  17338  sgrp2rid2  18029  grpidinv2  18096  gsumval3lem1  18954  dvdsrzring  20558  cncnp2  21817  vitalilem1  24136  aaliou3lem2  24859  2sqreulem1  25949  2sqreunnlem1  25952  pntibndlem2  26094  tgjustf  26186  iscgrglt  26227  islnoppd  26453  oppcom  26457  opphllem1  26460  opphllem5  26464  oppperpex  26466  hpgerlem  26478  colhp  26483  ax5seg  26651  uhgr2edg  26917  nbupgrres  27073  usgr2pthlem  27471  crctcshwlkn0lem5  27519  clwwlknonwwlknonb  27812  1pthond  27850  3pthdlem1  27870  frgrwopreglem5a  28017  grpoidinv  28212  nmcvcn  28399  leopmul  29838  resf1o  30392  trsp2cyc  30692  rhmopp  30819  oddpwdc  31511  poseq  32992  btwnconn1  33459  finminlem  33563  ptrecube  34773  poimirlem22  34795  isrngod  35057  paddasslem4  36839  cdleme21h  37350  cdleme26eALTN  37377  cdleme40m  37483  cdlemf2  37578  dicssdvh  38202  dihopelvalcpre  38264  dihmeetlem4preN  38322  dih1dimatlem0  38344  lzenom  39245  jm2.27c  39482  clrellem  39860  2pm13.193  40763  disjxp1  41208  dmrelrnrel  41366  infleinflem2  41515  mullimc  41773  mullimcf  41780  addlimc  41805  0ellimcdiv  41806  icccncfext  42046  stoweidlem52  42214  wallispilem4  42230  fourierdlem16  42285  fourierdlem21  42290  fourierdlem48  42316  fourierdlem51  42319  fourierdlem52  42320  fourierdlem54  42322  fourierdlem64  42332  fourierdlem76  42344  fourierdlem77  42345  fourierdlem80  42348  fourierdlem86  42354  fourierdlem87  42355  fourierdlem102  42370  fourierdlem114  42382  sge0f1o  42541  sge0split  42568  nnfoctbdjlem  42614  iundjiun  42619  ismeannd  42626  psmeasure  42630  isomennd  42690  hoidmvle  42759  ovncvr2  42770  dfatbrafv2b  43321  oexpnegnz  43720  rngcinv  44180  rngcinvALTV  44192  ringcinv  44231  ringcinvALTV  44255  itsclc0b  44687
  Copyright terms: Public domain W3C validator