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

Theorem jctir 545
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 539 1  |-  ( ph  ->  ( ps  /\  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  jctr  549  uniintsn  4285  ordunidif  5489  funtp  5652  foimacnv  5853  respreima  6031  fpr  6095  curry1  6914  dmtpos  7010  wfrlem13  7073  tfrlem10  7130  oawordeulem  7280  oelim2  7321  oaabs2  7371  ixpsnf1o  7587  ssdomg  7640  fodomr  7748  limenpsi  7772  cantnfrescl  8206  cardprclem  8438  fin4en1  8764  ssfin4  8765  axdc3lem2  8906  axdc3lem4  8908  fpwwe2lem9  9088  gruina  9268  reclem2pr  9498  recexsrlem  9552  nn0n0n1ge2b  10961  xmulpnf1  11588  ige2m2fzo  12007  swrdlsw  12844  swrd2lsw  13075  climeu  13667  odd2np1  14413  algcvgblem  14584  lcmfass  14667  qredeu  14712  qnumdencoprm  14742  qeqnumdivden  14743  isacs1i  15611  subgga  17002  symgfixf1  17126  sylow1lem2  17299  sylow3lem1  17327  nn0gsumfz  17661  mptcoe1fsupp  18856  evls1gsumadd  18961  evls1gsummul  18962  evl1gsummul  18996  mat1scmat  19612  smadiadetlem4  19742  mptcoe1matfsupp  19874  chfacfscmulgsum  19932  chfacfpmmulgsum  19936  eltg3i  20024  topbas  20036  neips  20177  restntr  20246  lmbrf  20324  cmpcld  20465  rnelfm  21016  tsmsres  21206  reconnlem1  21892  lmmbrf  22280  iscauf  22298  caucfil  22301  cmetcaulem  22306  ovolctb2  22493  voliunlem1  22551  isosctrlem1  23795  bcmono  24253  dchrvmasumlem2  24384  mulog2sumlem2  24421  pntlemb  24483  axlowdimlem13  25032  2pthon3v  25382  wlkdvspthlem  25385  constr3cycl  25437  0clwlk  25541  clwlkisclwwlklem2fv2  25559  clwlkf1clwwlk  25626  clwlksizeeq  25628  frghash2spot  25839  extwwlkfablem2  25854  numclwwlk6  25889  grpofo  25975  rngoideu  26160  nvss  26260  nmosetn0  26454  hhsst  26965  pjoc1i  27132  chlejb1i  27177  cmbr4i  27302  pjjsi  27401  nmopun  27715  stlesi  27942  mdsl2bi  28024  mdslmd1lem1  28026  xraddge02  28384  supxrnemnf  28402  qtopt1  28710  lmxrge0  28806  esumcst  28932  sigagenval  29010  measdivcstOLD  29094  oms0  29173  oms0OLD  29177  ballotlemfc0  29373  ballotlemfcc  29374  bnj945  29633  bnj150  29735  bnj986  29813  bnj1421  29899  dftrpred3g  30522  nodense  30626  nobndup  30637  fness  31053  nandsym1  31130  bj-finsumval0  31746  finixpnum  31974  poimirlem3  31987  poimirlem16  32000  poimirlem17  32001  poimirlem19  32003  poimirlem20  32004  poimirlem27  32011  mblfinlem3  32023  ismblfin  32025  lcvexchlem5  32648  paddssat  33423  dibn0  34765  lclkrs2  35152  fiphp3d  35706  pellqrex  35770  jm2.16nn0  35903  rp-fakeanorass  36201  rfcnpre1  37379  icccncfext  37802  wallispilem4  37967  stgoldbwt  38914  bgoldbwt  38915  bgoldbst  38916  evengpoap3  38931  wtgoldbnnsum4prm  38934  bgoldbnnsum3prm  38936  2pthon3v-av  39891  usgra2pthlem1  39939  ply1mulgsumlem2  40451  ldepspr  40538  blennngt2o2  40675
  Copyright terms: Public domain W3C validator