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  1927  uniintsn  3899  ordunidif  4440  funtp  5303  foimacnv  5490  respreima  5654  fpr  5704  curry1  6210  dmtpos  6246  tfrlem10  6403  oawordeulem  6552  oelim2  6593  oaabs2  6643  ixpsnf1o  6856  ssdomg  6907  fodomr  7012  limenpsi  7036  cardprclem  7612  fin4en1  7935  ssfin4  7936  axdc3lem2  8077  axdc3lem4  8079  fpwwe2lem9  8260  gruina  8440  reclem2pr  8672  recexsrlem  8725  xmulpnf1  10594  climeu  12029  odd2np1  12587  algcvgblem  12747  qredeu  12786  qnumdencoprm  12816  qeqnumdivden  12817  isacs1i  13559  subgga  14754  sylow1lem2  14910  sylow3lem1  14938  eltg3i  16699  topbas  16710  neips  16850  restntr  16912  lmbrf  16990  cmpcld  17129  rnelfm  17648  reconnlem1  18331  lmmbrf  18688  iscauf  18706  caucfil  18709  cmetcaulem  18714  ovolctb2  18851  voliunlem1  18907  isosctrlem1  20118  bcmono  20516  dchrvmasumlem2  20647  mulog2sumlem2  20684  pntlemb  20746  grpofo  20866  rngoideu  21051  nvss  21149  nmosetn0  21343  hhsst  21843  pjoc1i  22010  chlejb1i  22055  cmbr4i  22180  pjjsi  22279  nmopun  22594  stlesi  22821  mdsl2bi  22903  mdslmd1lem1  22905  ballotlemfc0  23051  ballotlemfcc  23052  xraddge02  23252  lmxrge0  23375  esumcst  23436  sigagenval  23501  measdivcstOLD  23551  measdivcst  23552  relexpsucr  24026  dftrpred3g  24236  wfrlem13  24268  nodense  24343  nobndup  24354  axlowdimlem13  24582  nandsym1  24861  trooo  25394  osneisi  25531  indcls2  25996  fness  26282  fiphp3d  26902  pellqrex  26964  stoweidlem53  27802  wallispilem4  27817  stirlinglem15  27837  bnj945  28805  bnj150  28908  bnj986  28986  bnj1421  29072  lcvexchlem5  29228  paddssat  30003  dibn0  31343  lclkrs2  31730
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