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  4229  ordunidif  5426  funtp  5589  foimacnv  5784  respreima  5961  fpr  6024  curry1  6836  dmtpos  6933  wfrlem13  6996  tfrlem10  7053  oawordeulem  7203  oelim2  7244  oaabs2  7294  ixpsnf1o  7510  ssdomg  7562  fodomr  7669  limenpsi  7693  cantnfrescl  8126  cardprclem  8358  fin4en1  8683  ssfin4  8684  axdc3lem2  8825  axdc3lem4  8827  fpwwe2lem9  9007  gruina  9187  reclem2pr  9417  recexsrlem  9471  nn0n0n1ge2b  10877  xmulpnf1  11504  ige2m2fzo  11920  swrdlsw  12747  swrd2lsw  12964  climeu  13555  odd2np1  14301  algcvgblem  14472  lcmfass  14555  qredeu  14600  qnumdencoprm  14630  qeqnumdivden  14631  isacs1i  15499  subgga  16890  symgfixf1  17014  sylow1lem2  17187  sylow3lem1  17215  nn0gsumfz  17549  mptcoe1fsupp  18744  evls1gsumadd  18849  evls1gsummul  18850  evl1gsummul  18884  mat1scmat  19499  smadiadetlem4  19629  mptcoe1matfsupp  19761  chfacfscmulgsum  19819  chfacfpmmulgsum  19823  eltg3i  19911  topbas  19923  neips  20064  restntr  20133  lmbrf  20211  cmpcld  20352  rnelfm  20903  tsmsres  21093  reconnlem1  21779  lmmbrf  22167  iscauf  22185  caucfil  22188  cmetcaulem  22193  ovolctb2  22380  voliunlem1  22438  isosctrlem1  23682  bcmono  24140  dchrvmasumlem2  24271  mulog2sumlem2  24308  pntlemb  24370  axlowdimlem13  24919  2pthon3v  25269  wlkdvspthlem  25272  constr3cycl  25324  0clwlk  25428  clwlkisclwwlklem2fv2  25446  clwlkf1clwwlk  25513  clwlksizeeq  25515  frghash2spot  25726  extwwlkfablem2  25741  numclwwlk6  25776  grpofo  25862  rngoideu  26047  nvss  26147  nmosetn0  26341  hhsst  26852  pjoc1i  27019  chlejb1i  27064  cmbr4i  27189  pjjsi  27288  nmopun  27602  stlesi  27829  mdsl2bi  27911  mdslmd1lem1  27913  xraddge02  28279  supxrnemnf  28297  qtopt1  28607  lmxrge0  28703  esumcst  28829  sigagenval  28907  measdivcstOLD  28991  oms0  29070  oms0OLD  29074  ballotlemfc0  29270  ballotlemfcc  29271  bnj945  29530  bnj150  29632  bnj986  29710  bnj1421  29796  dftrpred3g  30418  nodense  30520  nobndup  30531  fness  30947  nandsym1  31024  bj-finsumval0  31603  finixpnum  31831  poimirlem3  31844  poimirlem16  31857  poimirlem17  31858  poimirlem19  31860  poimirlem20  31861  poimirlem27  31868  mblfinlem3  31880  ismblfin  31882  lcvexchlem5  32510  paddssat  33285  dibn0  34627  lclkrs2  35014  fiphp3d  35568  pellqrex  35633  jm2.16nn0  35766  rp-fakeanorass  36064  rfcnpre1  37250  icccncfext  37642  wallispilem4  37807  stgoldbwt  38684  bgoldbwt  38685  bgoldbst  38686  evengpoap3  38701  wtgoldbnnsum4prm  38704  bgoldbnnsum3prm  38706  usgra2pthlem1  39252  ply1mulgsumlem2  39766  ldepspr  39853  blennngt2o2  39990
  Copyright terms: Public domain W3C validator