MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jctir Unicode version

Theorem jctir 524
Description: Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
Hypotheses
Ref Expression
jctil.1  |-  ( ph  ->  ps )
jctil.2  |-  ch
Assertion
Ref Expression
jctir  |-  ( ph  ->  ( ps  /\  ch ) )

Proof of Theorem jctir
StepHypRef Expression
1 jctil.1 . 2  |-  ( ph  ->  ps )
2 jctil.2 . . 3  |-  ch
32a1i 10 . 2  |-  ( ph  ->  ch )
41, 3jca 518 1  |-  ( ph  ->  ( ps  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  jctr  526  equvini  1940  uniintsn  3915  ordunidif  4456  funtp  5319  foimacnv  5506  respreima  5670  fpr  5720  curry1  6226  dmtpos  6262  tfrlem10  6419  oawordeulem  6568  oelim2  6609  oaabs2  6659  ixpsnf1o  6872  ssdomg  6923  fodomr  7028  limenpsi  7052  cardprclem  7628  fin4en1  7951  ssfin4  7952  axdc3lem2  8093  axdc3lem4  8095  fpwwe2lem9  8276  gruina  8456  reclem2pr  8688  recexsrlem  8741  xmulpnf1  10610  climeu  12045  odd2np1  12603  algcvgblem  12763  qredeu  12802  qnumdencoprm  12832  qeqnumdivden  12833  isacs1i  13575  subgga  14770  sylow1lem2  14926  sylow3lem1  14954  eltg3i  16715  topbas  16726  neips  16866  restntr  16928  lmbrf  17006  cmpcld  17145  rnelfm  17664  reconnlem1  18347  lmmbrf  18704  iscauf  18722  caucfil  18725  cmetcaulem  18730  ovolctb2  18867  voliunlem1  18923  isosctrlem1  20134  bcmono  20532  dchrvmasumlem2  20663  mulog2sumlem2  20700  pntlemb  20762  grpofo  20882  rngoideu  21067  nvss  21165  nmosetn0  21359  hhsst  21859  pjoc1i  22026  chlejb1i  22071  cmbr4i  22196  pjjsi  22295  nmopun  22610  stlesi  22837  mdsl2bi  22919  mdslmd1lem1  22921  ballotlemfc0  23067  ballotlemfcc  23068  xraddge02  23267  lmxrge0  23390  esumcst  23451  sigagenval  23516  measdivcstOLD  23566  measdivcst  23567  relexpsucr  24041  dftrpred3g  24307  wfrlem13  24339  nodense  24414  nobndup  24425  axlowdimlem13  24654  nandsym1  24933  trooo  25497  osneisi  25634  indcls2  26099  fness  26385  fiphp3d  27005  pellqrex  27067  stoweidlem53  27905  wallispilem4  27920  stirlinglem15  27940  wlkdvspthlem  28365  constr3cycl  28407  bnj945  29121  bnj150  29224  bnj986  29302  bnj1421  29388  equviniNEW7  29502  lcvexchlem5  29850  paddssat  30625  dibn0  31965  lclkrs2  32352
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator