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

Theorem jctir 525
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 519 1  |-  ( ph  ->  ( ps  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  jctr  527  equvini  2013  uniintsn  4022  ordunidif  4563  funtp  5436  foimacnv  5625  respreima  5791  fpr  5846  curry1  6370  dmtpos  6420  tfrlem10  6577  oawordeulem  6726  oelim2  6767  oaabs2  6817  ixpsnf1o  7031  ssdomg  7082  fodomr  7187  limenpsi  7211  cardprclem  7792  fin4en1  8115  ssfin4  8116  axdc3lem2  8257  axdc3lem4  8259  fpwwe2lem9  8439  gruina  8619  reclem2pr  8851  recexsrlem  8904  nn0n0n1ge2b  10206  xmulpnf1  10778  climeu  12269  odd2np1  12828  algcvgblem  12988  qredeu  13027  qnumdencoprm  13057  qeqnumdivden  13058  isacs1i  13802  subgga  14997  sylow1lem2  15153  sylow3lem1  15181  eltg3i  16942  topbas  16953  neips  17093  restntr  17161  lmbrf  17239  cmpcld  17380  rnelfm  17899  reconnlem1  18721  lmmbrf  19079  iscauf  19097  caucfil  19100  cmetcaulem  19105  ovolctb2  19248  voliunlem1  19304  isosctrlem1  20522  bcmono  20921  dchrvmasumlem2  21052  mulog2sumlem2  21089  pntlemb  21151  2pthon3v  21445  wlkdvspthlem  21448  constr3cycl  21489  grpofo  21628  rngoideu  21813  nvss  21913  nmosetn0  22107  hhsst  22607  pjoc1i  22774  chlejb1i  22819  cmbr4i  22944  pjjsi  23043  nmopun  23358  stlesi  23585  mdsl2bi  23667  mdslmd1lem1  23669  xraddge02  23952  supxrnemnf  23956  lmxrge0  24134  esumcst  24244  sigagenval  24312  measdivcstOLD  24365  ballotlemfc0  24522  ballotlemfcc  24523  relexpsucr  24902  dftrpred3g  25253  wfrlem13  25285  nodense  25360  nobndup  25371  axlowdimlem13  25600  nandsym1  25879  fness  26046  fiphp3d  26564  pellqrex  26626  rfcnpre1  27351  wallispilem4  27478  bnj945  28475  bnj150  28578  bnj986  28656  bnj1421  28742  equviniNEW7  28856  lcvexchlem5  29204  paddssat  29979  dibn0  31319  lclkrs2  31706
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator