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

Theorem jctir 536
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 530 1  |-  ( ph  ->  ( ps  /\  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  jctr  540  uniintsn  4309  ordunidif  4915  funtp  5622  foimacnv  5815  respreima  5992  fpr  6055  curry1  6865  dmtpos  6959  tfrlem10  7048  oawordeulem  7195  oelim2  7236  oaabs2  7286  ixpsnf1o  7502  ssdomg  7554  fodomr  7661  limenpsi  7685  cantnfrescl  8086  cardprclem  8351  fin4en1  8680  ssfin4  8681  axdc3lem2  8822  axdc3lem4  8824  fpwwe2lem9  9005  gruina  9185  reclem2pr  9415  recexsrlem  9469  nn0n0n1ge2b  10856  xmulpnf1  11469  ige2m2fzo  11860  swrdlsw  12671  swrd2lsw  12884  climeu  13463  odd2np1  14133  algcvgblem  14293  qredeu  14335  qnumdencoprm  14365  qeqnumdivden  14366  isacs1i  15149  subgga  16540  symgfixf1  16664  sylow1lem2  16821  sylow3lem1  16849  nn0gsumfz  17210  mptcoe1fsupp  18453  evls1gsumadd  18559  evls1gsummul  18560  evl1gsummul  18594  mat1scmat  19211  smadiadetlem4  19341  mptcoe1matfsupp  19473  chfacfscmulgsum  19531  chfacfpmmulgsum  19535  eltg3i  19632  topbas  19644  neips  19784  restntr  19853  lmbrf  19931  cmpcld  20072  rnelfm  20623  tsmsres  20815  reconnlem1  21500  lmmbrf  21870  iscauf  21888  caucfil  21891  cmetcaulem  21896  ovolctb2  22072  voliunlem1  22129  isosctrlem1  23352  bcmono  23753  dchrvmasumlem2  23884  mulog2sumlem2  23921  pntlemb  23983  axlowdimlem13  24462  2pthon3v  24811  wlkdvspthlem  24814  constr3cycl  24866  0clwlk  24970  clwlkisclwwlklem2fv2  24988  clwlkf1clwwlk  25055  clwlksizeeq  25057  frghash2spot  25268  extwwlkfablem2  25283  numclwwlk6  25318  grpofo  25402  rngoideu  25587  nvss  25687  nmosetn0  25881  hhsst  26383  pjoc1i  26550  chlejb1i  26595  cmbr4i  26720  pjjsi  26819  nmopun  27134  stlesi  27361  mdsl2bi  27443  mdslmd1lem1  27445  xraddge02  27811  supxrnemnf  27820  qtopt1  28076  lmxrge0  28172  esumcst  28295  sigagenval  28373  measdivcstOLD  28435  oms0  28508  ballotlemfc0  28698  ballotlemfcc  28699  dftrpred3g  29559  wfrlem13  29598  nodense  29692  nobndup  29703  nandsym1  30118  finixpnum  30281  mblfinlem3  30296  ismblfin  30298  fness  30410  fiphp3d  30995  pellqrex  31057  jm2.16nn0  31188  rfcnpre1  31637  icccncfext  31932  wallispilem4  32092  usgra2pthlem1  32744  ply1mulgsumlem2  33260  ldepspr  33347  blennngt2o2  33486  bnj945  34252  bnj150  34354  bnj986  34432  bnj1421  34518  bj-finsumval0  35082  lcvexchlem5  35179  paddssat  35954  dibn0  37296  lclkrs2  37683  rp-fakeanorass  38170
  Copyright terms: Public domain W3C validator