MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jctir Structured version   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  2079  equviniOLD  2080  uniintsn  4080  ordunidif  4622  funtp  5496  foimacnv  5685  respreima  5852  fpr  5907  curry1  6431  dmtpos  6484  tfrlem10  6641  oawordeulem  6790  oelim2  6831  oaabs2  6881  ixpsnf1o  7095  ssdomg  7146  fodomr  7251  limenpsi  7275  cardprclem  7859  fin4en1  8182  ssfin4  8183  axdc3lem2  8324  axdc3lem4  8326  fpwwe2lem9  8506  gruina  8686  reclem2pr  8918  recexsrlem  8971  nn0n0n1ge2b  10274  xmulpnf1  10846  climeu  12342  odd2np1  12901  algcvgblem  13061  qredeu  13100  qnumdencoprm  13130  qeqnumdivden  13131  isacs1i  13875  subgga  15070  sylow1lem2  15226  sylow3lem1  15254  eltg3i  17019  topbas  17030  neips  17170  restntr  17239  lmbrf  17317  cmpcld  17458  rnelfm  17978  reconnlem1  18850  lmmbrf  19208  iscauf  19226  caucfil  19229  cmetcaulem  19234  ovolctb2  19381  voliunlem1  19437  isosctrlem1  20655  bcmono  21054  dchrvmasumlem2  21185  mulog2sumlem2  21222  pntlemb  21284  2pthon3v  21597  wlkdvspthlem  21600  constr3cycl  21641  grpofo  21780  rngoideu  21965  nvss  22065  nmosetn0  22259  hhsst  22759  pjoc1i  22926  chlejb1i  22971  cmbr4i  23096  pjjsi  23195  nmopun  23510  stlesi  23737  mdsl2bi  23819  mdslmd1lem1  23821  xraddge02  24116  supxrnemnf  24120  lmxrge0  24330  esumcst  24448  sigagenval  24516  measdivcstOLD  24571  ballotlemfc0  24743  ballotlemfcc  24744  relexpsucr  25123  dftrpred3g  25504  wfrlem13  25543  nodense  25637  nobndup  25648  axlowdimlem13  25886  nandsym1  26165  mblfinlem2  26236  ismblfin  26238  fness  26354  fiphp3d  26872  pellqrex  26934  rfcnpre1  27658  wallispilem4  27785  usgra2pthlem1  28264  frghash2spot  28390  bnj945  29082  bnj150  29185  bnj986  29263  bnj1421  29349  equviniNEW7  29465  lcvexchlem5  29774  paddssat  30549  dibn0  31889  lclkrs2  32276
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