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  4305  ordunidif  4912  funtp  5626  foimacnv  5819  respreima  5997  fpr  6060  curry1  6873  dmtpos  6965  tfrlem10  7054  oawordeulem  7201  oelim2  7242  oaabs2  7292  ixpsnf1o  7507  ssdomg  7559  fodomr  7666  limenpsi  7690  cantnfrescl  8093  cardprclem  8358  fin4en1  8687  ssfin4  8688  axdc3lem2  8829  axdc3lem4  8831  fpwwe2lem9  9014  gruina  9194  reclem2pr  9424  recexsrlem  9478  nn0n0n1ge2b  10861  xmulpnf1  11470  ige2m2fzo  11853  swrdlsw  12651  swrd2lsw  12864  climeu  13352  odd2np1  13918  algcvgblem  14078  qredeu  14120  qnumdencoprm  14150  qeqnumdivden  14151  isacs1i  14926  subgga  16207  symgfixf1  16331  sylow1lem2  16488  sylow3lem1  16516  nn0gsumfz  16881  mptcoe1fsupp  18123  evls1gsumadd  18229  evls1gsummul  18230  evl1gsummul  18264  mat1scmat  18908  smadiadetlem4  19038  mptcoe1matfsupp  19170  chfacfscmulgsum  19228  chfacfpmmulgsum  19232  eltg3i  19329  topbas  19340  neips  19480  restntr  19549  lmbrf  19627  cmpcld  19768  rnelfm  20320  tsmsres  20512  reconnlem1  21197  lmmbrf  21567  iscauf  21585  caucfil  21588  cmetcaulem  21593  ovolctb2  21769  voliunlem1  21826  isosctrlem1  23017  bcmono  23417  dchrvmasumlem2  23548  mulog2sumlem2  23585  pntlemb  23647  axlowdimlem13  24122  2pthon3v  24471  wlkdvspthlem  24474  constr3cycl  24526  0clwlk  24630  clwlkisclwwlklem2fv2  24648  clwlkf1clwwlk  24715  clwlksizeeq  24717  frghash2spot  24928  extwwlkfablem2  24943  numclwwlk6  24978  grpofo  25066  rngoideu  25251  nvss  25351  nmosetn0  25545  hhsst  26047  pjoc1i  26214  chlejb1i  26259  cmbr4i  26384  pjjsi  26483  nmopun  26798  stlesi  27025  mdsl2bi  27107  mdslmd1lem1  27109  xraddge02  27442  supxrnemnf  27448  qtopt1  27704  lmxrge0  27800  esumcst  27937  sigagenval  28006  measdivcstOLD  28061  ballotlemfc0  28297  ballotlemfcc  28298  relexpsucr  28919  dftrpred3g  29284  wfrlem13  29323  nodense  29417  nobndup  29428  nandsym1  29855  finixpnum  30006  mblfinlem3  30021  ismblfin  30023  fness  30135  fiphp3d  30721  pellqrex  30783  jm2.16nn0  30914  rfcnpre1  31341  icccncfext  31593  wallispilem4  31735  usgra2pthlem1  32187  ply1mulgsumlem2  32697  ldepspr  32784  bnj945  33539  bnj150  33641  bnj986  33719  bnj1421  33805  bj-finsumval0  34365  lcvexchlem5  34465  paddssat  35240  dibn0  36582  lclkrs2  36969  rp-fakeanorass  37402
  Copyright terms: Public domain W3C validator