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

Theorem jctir 538
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 532 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  542  uniintsn  4165  ordunidif  4767  funtp  5470  foimacnv  5658  respreima  5832  fpr  5890  curry1  6664  dmtpos  6757  tfrlem10  6846  oawordeulem  6993  oelim2  7034  oaabs2  7084  ixpsnf1o  7303  ssdomg  7355  fodomr  7462  limenpsi  7486  cantnfrescl  7884  cardprclem  8149  fin4en1  8478  ssfin4  8479  axdc3lem2  8620  axdc3lem4  8622  fpwwe2lem9  8805  gruina  8985  reclem2pr  9217  recexsrlem  9270  nn0n0n1ge2b  10644  xmulpnf1  11237  swrdlsw  12346  swrd2lsw  12552  climeu  13033  odd2np1  13592  algcvgblem  13752  qredeu  13793  qnumdencoprm  13823  qeqnumdivden  13824  isacs1i  14595  subgga  15818  symgfixf1  15943  sylow1lem2  16098  sylow3lem1  16126  evls1gsummul  17760  evl1gsummul  17794  smadiadetlem4  18475  eltg3i  18566  topbas  18577  neips  18717  restntr  18786  lmbrf  18864  cmpcld  19005  rnelfm  19526  tsmsres  19718  reconnlem1  20403  lmmbrf  20773  iscauf  20791  caucfil  20794  cmetcaulem  20799  ovolctb2  20975  voliunlem1  21031  isosctrlem1  22216  bcmono  22616  dchrvmasumlem2  22747  mulog2sumlem2  22784  pntlemb  22846  axlowdimlem13  23200  2pthon3v  23503  wlkdvspthlem  23506  constr3cycl  23547  grpofo  23686  rngoideu  23871  nvss  23971  nmosetn0  24165  hhsst  24667  pjoc1i  24834  chlejb1i  24879  cmbr4i  25004  pjjsi  25103  nmopun  25418  stlesi  25645  mdsl2bi  25727  mdslmd1lem1  25729  xraddge02  26050  supxrnemnf  26056  lmxrge0  26382  esumcst  26514  sigagenval  26583  measdivcstOLD  26638  ballotlemfc0  26875  ballotlemfcc  26876  relexpsucr  27332  dftrpred3g  27697  wfrlem13  27736  nodense  27830  nobndup  27841  nandsym1  28268  finixpnum  28414  mblfinlem3  28430  ismblfin  28432  fness  28554  fiphp3d  29158  pellqrex  29220  rfcnpre1  29741  wallispilem4  29863  ige2m2fzo  30220  usgra2pthlem1  30300  0clwlk  30428  clwlkisclwwlklem2fv2  30445  clwlkf1clwwlk  30523  clwlksizeeq  30525  frghash2spot  30656  extwwlkfablem2  30671  numclwwlk6  30706  nn0gsumfz  30804  mptcoe1fsupp  30833  ply1mulgsumlem2  30845  mptcoe1matfsupp  30891  ldepspr  31007  bnj945  31767  bnj150  31869  bnj986  31947  bnj1421  32033  bj-finsumval0  32583  lcvexchlem5  32683  paddssat  33458  dibn0  34798  lclkrs2  35185
  Copyright terms: Public domain W3C validator