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

Theorem jctir 540
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 534 1  |-  ( ph  ->  ( ps  /\  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  jctr  544  uniintsn  4296  ordunidif  5490  funtp  5653  foimacnv  5848  respreima  6024  fpr  6087  curry1  6899  dmtpos  6993  wfrlem13  7056  tfrlem10  7113  oawordeulem  7263  oelim2  7304  oaabs2  7354  ixpsnf1o  7570  ssdomg  7622  fodomr  7729  limenpsi  7753  cantnfrescl  8180  cardprclem  8412  fin4en1  8737  ssfin4  8738  axdc3lem2  8879  axdc3lem4  8881  fpwwe2lem9  9062  gruina  9242  reclem2pr  9472  recexsrlem  9526  nn0n0n1ge2b  10933  xmulpnf1  11560  ige2m2fzo  11974  swrdlsw  12793  swrd2lsw  13006  climeu  13597  odd2np1  14343  algcvgblem  14507  lcmfass  14590  qredeu  14635  qnumdencoprm  14665  qeqnumdivden  14666  isacs1i  15514  subgga  16905  symgfixf1  17029  sylow1lem2  17186  sylow3lem1  17214  nn0gsumfz  17548  mptcoe1fsupp  18743  evls1gsumadd  18848  evls1gsummul  18849  evl1gsummul  18883  mat1scmat  19495  smadiadetlem4  19625  mptcoe1matfsupp  19757  chfacfscmulgsum  19815  chfacfpmmulgsum  19819  eltg3i  19907  topbas  19919  neips  20060  restntr  20129  lmbrf  20207  cmpcld  20348  rnelfm  20899  tsmsres  21089  reconnlem1  21755  lmmbrf  22125  iscauf  22143  caucfil  22146  cmetcaulem  22151  ovolctb2  22323  voliunlem1  22380  isosctrlem1  23612  bcmono  24068  dchrvmasumlem2  24199  mulog2sumlem2  24236  pntlemb  24298  axlowdimlem13  24830  2pthon3v  25179  wlkdvspthlem  25182  constr3cycl  25234  0clwlk  25338  clwlkisclwwlklem2fv2  25356  clwlkf1clwwlk  25423  clwlksizeeq  25425  frghash2spot  25636  extwwlkfablem2  25651  numclwwlk6  25686  grpofo  25772  rngoideu  25957  nvss  26057  nmosetn0  26251  hhsst  26752  pjoc1i  26919  chlejb1i  26964  cmbr4i  27089  pjjsi  27188  nmopun  27502  stlesi  27729  mdsl2bi  27811  mdslmd1lem1  27813  xraddge02  28177  supxrnemnf  28190  qtopt1  28501  lmxrge0  28597  esumcst  28723  sigagenval  28801  measdivcstOLD  28885  oms0  28958  ballotlemfc0  29151  ballotlemfcc  29152  bnj945  29373  bnj150  29475  bnj986  29553  bnj1421  29639  dftrpred3g  30261  nodense  30363  nobndup  30374  fness  30790  nandsym1  30867  bj-finsumval0  31447  finixpnum  31634  poimirlem3  31647  poimirlem16  31660  poimirlem17  31661  poimirlem19  31663  poimirlem20  31664  poimirlem27  31671  mblfinlem3  31683  ismblfin  31685  lcvexchlem5  32313  paddssat  33088  dibn0  34430  lclkrs2  34817  fiphp3d  35371  pellqrex  35433  jm2.16nn0  35565  rp-fakeanorass  35856  rfcnpre1  36980  icccncfext  37337  wallispilem4  37499  stgoldbwt  38267  bgoldbwt  38268  bgoldbst  38269  evengpoap3  38284  wtgoldbnnsum4prm  38287  bgoldbnnsum3prm  38289  usgra2pthlem1  38423  ply1mulgsumlem2  38939  ldepspr  39026  blennngt2o2  39164
  Copyright terms: Public domain W3C validator