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

Theorem jctir 535
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 529 1  |-  ( ph  ->  ( ps  /\  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  jctr  539  uniintsn  4155  ordunidif  4756  funtp  5460  foimacnv  5648  respreima  5822  fpr  5879  curry1  6655  dmtpos  6748  tfrlem10  6834  oawordeulem  6983  oelim2  7024  oaabs2  7074  ixpsnf1o  7293  ssdomg  7345  fodomr  7452  limenpsi  7476  cantnfrescl  7874  cardprclem  8139  fin4en1  8468  ssfin4  8469  axdc3lem2  8610  axdc3lem4  8612  fpwwe2lem9  8795  gruina  8975  reclem2pr  9207  recexsrlem  9260  nn0n0n1ge2b  10634  xmulpnf1  11227  swrdlsw  12332  swrd2lsw  12538  climeu  13019  odd2np1  13577  algcvgblem  13737  qredeu  13778  qnumdencoprm  13808  qeqnumdivden  13809  isacs1i  14580  subgga  15800  symgfixf1  15925  sylow1lem2  16080  sylow3lem1  16108  smadiadetlem4  18319  eltg3i  18410  topbas  18421  neips  18561  restntr  18630  lmbrf  18708  cmpcld  18849  rnelfm  19370  tsmsres  19562  reconnlem1  20247  lmmbrf  20617  iscauf  20635  caucfil  20638  cmetcaulem  20643  ovolctb2  20819  voliunlem1  20875  isosctrlem1  22103  bcmono  22503  dchrvmasumlem2  22634  mulog2sumlem2  22671  pntlemb  22733  axlowdimlem13  23025  2pthon3v  23328  wlkdvspthlem  23331  constr3cycl  23372  grpofo  23511  rngoideu  23696  nvss  23796  nmosetn0  23990  hhsst  24492  pjoc1i  24659  chlejb1i  24704  cmbr4i  24829  pjjsi  24928  nmopun  25243  stlesi  25470  mdsl2bi  25552  mdslmd1lem1  25554  xraddge02  25877  supxrnemnf  25881  lmxrge0  26238  esumcst  26370  sigagenval  26439  measdivcstOLD  26494  ballotlemfc0  26725  ballotlemfcc  26726  relexpsucr  27181  dftrpred3g  27546  wfrlem13  27585  nodense  27679  nobndup  27690  nandsym1  28118  finixpnum  28260  mblfinlem3  28276  ismblfin  28278  fness  28400  fiphp3d  29005  pellqrex  29067  areaquad  29439  rfcnpre1  29588  wallispilem4  29711  ige2m2fzo  30068  usgra2pthlem1  30148  0clwlk  30276  clwlkisclwwlklem2fv2  30293  clwlkf1clwwlk  30371  clwlksizeeq  30373  frghash2spot  30504  extwwlkfablem2  30519  numclwwlk6  30554  ldepspr  30756  bnj945  31509  bnj150  31611  bnj986  31689  bnj1421  31775  bj-finsumval0  32199  lcvexchlem5  32296  paddssat  33071  dibn0  34411  lclkrs2  34798
  Copyright terms: Public domain W3C validator