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

Theorem jca31 556
 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 553 . 2 (𝜑 → (𝜓𝜒))
4 jca31.3 . 2 (𝜑𝜃)
53, 4jca 553 1 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 385 This theorem is referenced by:  3jca  1261  syl21anc  1365  xpdifid  5597  tpres  6507  f1oiso2  6642  oewordri  7717  boxriin  7992  cantnfrescl  8611  cfsuc  9117  genpcl  9868  ltexprlem5  9900  prsrlem1  9931  lemulge11  10923  lediv12a  10954  elnnz  11425  quoremz  12694  quoremnn0ALT  12696  fldiv  12699  modsumfzodifsn  12783  leexp1a  12959  faclbnd6  13126  wrdlen2i  13732  wwlktovfo  13747  setcinv  16787  sgrp2rid2  17460  grpidinv2  17521  mhmfmhm  17585  gsumval3lem1  18352  dvdsrzring  19879  scmatmhm  20388  cncnp2  21133  vitalilem1  23422  aaliou3lem2  24143  pntibndlem2  25325  iscgrglt  25454  islnoppd  25677  oppcom  25681  opphllem1  25684  opphllem5  25688  oppperpex  25690  hpgerlem  25702  colopp  25706  colhp  25707  ax5seg  25863  uhgr2edg  26145  nbupgrres  26310  usgr2pthlem  26715  crctcshwlkn0lem5  26762  wlknwwlksnsur  26844  wlkwwlksur  26851  clwwlknonwwlknonb  27080  clwwlknonwwlknonbOLD  27081  1pthond  27122  3pthdlem1  27142  frgrwopreglem5a  27291  grpoidinv  27490  nmcvcn  27678  leopmul  29121  resf1o  29633  rhmopp  29947  oddpwdc  30544  poseq  31878  btwnconn1  32333  finminlem  32437  bj-elid3  33217  ptrecube  33539  poimirlem22  33561  isrngod  33827  paddasslem4  35427  cdleme21h  35939  cdleme26eALTN  35966  cdleme40m  36072  cdlemf2  36167  dicssdvh  36792  dihopelvalcpre  36854  dihmeetlem4preN  36912  dih1dimatlem0  36934  lzenom  37650  jm2.27c  37891  clrellem  38246  2pm13.193  39085  disjxp1  39552  dmrelrnrel  39733  infleinflem2  39900  mullimc  40166  mullimcf  40173  addlimc  40198  0ellimcdiv  40199  cncfshift  40405  cncfperiod  40410  icccncfext  40418  stoweidlem52  40587  wallispilem4  40603  fourierdlem16  40658  fourierdlem21  40663  fourierdlem48  40689  fourierdlem51  40692  fourierdlem52  40693  fourierdlem54  40695  fourierdlem64  40705  fourierdlem76  40717  fourierdlem77  40718  fourierdlem80  40721  fourierdlem86  40727  fourierdlem87  40728  fourierdlem102  40743  fourierdlem114  40755  sge0f1o  40917  sge0split  40944  ismea  40986  nnfoctbdjlem  40990  iundjiun  40995  ismeannd  41002  psmeasure  41006  isomennd  41066  hoidmvle  41135  ovncvr2  41146  oexpnegnz  41914  rngcinv  42306  rngcinvALTV  42318  ringcinv  42357  ringcinvALTV  42381
 Copyright terms: Public domain W3C validator