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

Theorem jctir 525
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 11 . 2  |-  ( ph  ->  ch )
41, 3jca 519 1  |-  ( ph  ->  ( ps  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  jctr  527  equvini  2083  equviniOLD  2084  uniintsn  4087  ordunidif  4629  funtp  5503  foimacnv  5692  respreima  5859  fpr  5914  curry1  6438  dmtpos  6491  tfrlem10  6648  oawordeulem  6797  oelim2  6838  oaabs2  6888  ixpsnf1o  7102  ssdomg  7153  fodomr  7258  limenpsi  7282  cardprclem  7866  fin4en1  8189  ssfin4  8190  axdc3lem2  8331  axdc3lem4  8333  fpwwe2lem9  8513  gruina  8693  reclem2pr  8925  recexsrlem  8978  nn0n0n1ge2b  10281  xmulpnf1  10853  climeu  12349  odd2np1  12908  algcvgblem  13068  qredeu  13107  qnumdencoprm  13137  qeqnumdivden  13138  isacs1i  13882  subgga  15077  sylow1lem2  15233  sylow3lem1  15261  eltg3i  17026  topbas  17037  neips  17177  restntr  17246  lmbrf  17324  cmpcld  17465  rnelfm  17985  reconnlem1  18857  lmmbrf  19215  iscauf  19233  caucfil  19236  cmetcaulem  19241  ovolctb2  19388  voliunlem1  19444  isosctrlem1  20662  bcmono  21061  dchrvmasumlem2  21192  mulog2sumlem2  21229  pntlemb  21291  2pthon3v  21604  wlkdvspthlem  21607  constr3cycl  21648  grpofo  21787  rngoideu  21972  nvss  22072  nmosetn0  22266  hhsst  22766  pjoc1i  22933  chlejb1i  22978  cmbr4i  23103  pjjsi  23202  nmopun  23517  stlesi  23744  mdsl2bi  23826  mdslmd1lem1  23828  xraddge02  24123  supxrnemnf  24127  lmxrge0  24337  esumcst  24455  sigagenval  24523  measdivcstOLD  24578  ballotlemfc0  24750  ballotlemfcc  24751  relexpsucr  25130  dftrpred3g  25511  wfrlem13  25550  nodense  25644  nobndup  25655  axlowdimlem13  25893  nandsym1  26172  mblfinlem3  26245  ismblfin  26247  fness  26362  fiphp3d  26880  pellqrex  26942  rfcnpre1  27666  wallispilem4  27793  usgra2pthlem1  28310  frghash2spot  28452  bnj945  29144  bnj150  29247  bnj986  29325  bnj1421  29411  equviniNEW7  29527  lcvexchlem5  29836  paddssat  30611  dibn0  31951  lclkrs2  32338
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 178  df-an 361
  Copyright terms: Public domain W3C validator