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  2040  equviniOLD  2041  uniintsn  4047  ordunidif  4589  funtp  5462  foimacnv  5651  respreima  5818  fpr  5873  curry1  6397  dmtpos  6450  tfrlem10  6607  oawordeulem  6756  oelim2  6797  oaabs2  6847  ixpsnf1o  7061  ssdomg  7112  fodomr  7217  limenpsi  7241  cardprclem  7822  fin4en1  8145  ssfin4  8146  axdc3lem2  8287  axdc3lem4  8289  fpwwe2lem9  8469  gruina  8649  reclem2pr  8881  recexsrlem  8934  nn0n0n1ge2b  10237  xmulpnf1  10809  climeu  12304  odd2np1  12863  algcvgblem  13023  qredeu  13062  qnumdencoprm  13092  qeqnumdivden  13093  isacs1i  13837  subgga  15032  sylow1lem2  15188  sylow3lem1  15216  eltg3i  16981  topbas  16992  neips  17132  restntr  17200  lmbrf  17278  cmpcld  17419  rnelfm  17938  reconnlem1  18810  lmmbrf  19168  iscauf  19186  caucfil  19189  cmetcaulem  19194  ovolctb2  19341  voliunlem1  19397  isosctrlem1  20615  bcmono  21014  dchrvmasumlem2  21145  mulog2sumlem2  21182  pntlemb  21244  2pthon3v  21557  wlkdvspthlem  21560  constr3cycl  21601  grpofo  21740  rngoideu  21925  nvss  22025  nmosetn0  22219  hhsst  22719  pjoc1i  22886  chlejb1i  22931  cmbr4i  23056  pjjsi  23155  nmopun  23470  stlesi  23697  mdsl2bi  23779  mdslmd1lem1  23781  xraddge02  24076  supxrnemnf  24080  lmxrge0  24290  esumcst  24408  sigagenval  24476  measdivcstOLD  24531  ballotlemfc0  24703  ballotlemfcc  24704  relexpsucr  25083  dftrpred3g  25450  wfrlem13  25482  nodense  25557  nobndup  25568  axlowdimlem13  25797  nandsym1  26076  mblfinlem2  26144  ismblfin  26146  fness  26252  fiphp3d  26770  pellqrex  26832  rfcnpre1  27557  wallispilem4  27684  usgra2pthlem1  28040  frghash2spot  28166  bnj945  28850  bnj150  28953  bnj986  29031  bnj1421  29117  equviniNEW7  29231  lcvexchlem5  29521  paddssat  30296  dibn0  31636  lclkrs2  32023
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