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  4319  ordunidif  4926  funtp  5640  foimacnv  5833  respreima  6010  fpr  6069  curry1  6875  dmtpos  6967  tfrlem10  7056  oawordeulem  7203  oelim2  7244  oaabs2  7294  ixpsnf1o  7509  ssdomg  7561  fodomr  7668  limenpsi  7692  cantnfrescl  8095  cardprclem  8360  fin4en1  8689  ssfin4  8690  axdc3lem2  8831  axdc3lem4  8833  fpwwe2lem9  9016  gruina  9196  reclem2pr  9426  recexsrlem  9480  nn0n0n1ge2b  10860  xmulpnf1  11466  ige2m2fzo  11847  swrdlsw  12640  swrd2lsw  12853  climeu  13341  odd2np1  13905  algcvgblem  14065  qredeu  14107  qnumdencoprm  14137  qeqnumdivden  14138  isacs1i  14912  subgga  16143  symgfixf1  16268  sylow1lem2  16425  sylow3lem1  16453  nn0gsumfz  16815  mptcoe1fsupp  18054  evls1gsummul  18161  evl1gsummul  18195  mat1scmat  18836  smadiadetlem4  18966  mptcoe1matfsupp  19098  chfacfscmulgsum  19156  chfacfpmmulgsum  19160  eltg3i  19257  topbas  19268  neips  19408  restntr  19477  lmbrf  19555  cmpcld  19696  rnelfm  20217  tsmsres  20409  reconnlem1  21094  lmmbrf  21464  iscauf  21482  caucfil  21485  cmetcaulem  21490  ovolctb2  21666  voliunlem1  21723  isosctrlem1  22908  bcmono  23308  dchrvmasumlem2  23439  mulog2sumlem2  23476  pntlemb  23538  axlowdimlem13  23961  2pthon3v  24310  wlkdvspthlem  24313  constr3cycl  24365  0clwlk  24469  clwlkisclwwlklem2fv2  24487  clwlkf1clwwlk  24554  clwlksizeeq  24556  frghash2spot  24768  extwwlkfablem2  24783  numclwwlk6  24818  grpofo  24905  rngoideu  25090  nvss  25190  nmosetn0  25384  hhsst  25886  pjoc1i  26053  chlejb1i  26098  cmbr4i  26223  pjjsi  26322  nmopun  26637  stlesi  26864  mdsl2bi  26946  mdslmd1lem1  26948  xraddge02  27273  supxrnemnf  27279  lmxrge0  27598  qtopt1  27664  esumcst  27739  sigagenval  27808  measdivcstOLD  27863  ballotlemfc0  28099  ballotlemfcc  28100  relexpsucr  28556  dftrpred3g  28921  wfrlem13  28960  nodense  29054  nobndup  29065  nandsym1  29492  finixpnum  29643  mblfinlem3  29658  ismblfin  29660  fness  29782  fiphp3d  30385  pellqrex  30447  rfcnpre1  31000  icccncfext  31254  wallispilem4  31396  usgra2pthlem1  31848  ply1mulgsumlem2  32086  ldepspr  32173  bnj945  32929  bnj150  33031  bnj986  33109  bnj1421  33195  bj-finsumval0  33753  lcvexchlem5  33853  paddssat  34628  dibn0  35968  lclkrs2  36355
  Copyright terms: Public domain W3C validator