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

Theorem jctir 521
Description: Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
Hypotheses
Ref Expression
jctil.1 (𝜑𝜓)
jctil.2 𝜒
Assertion
Ref Expression
jctir (𝜑 → (𝜓𝜒))

Proof of Theorem jctir
StepHypRef Expression
1 jctil.1 . 2 (𝜑𝜓)
2 jctil.2 . . 3 𝜒
32a1i 11 . 2 (𝜑𝜒)
41, 3jca 512 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  jctr  525  ordunidif  6106  funtp  6273  dmtpos  7746  oaabs2  8113  ixpsnf1o  8340  fodomr  8505  mapfienlem2  8705  cantnfrescl  8974  cardprclem  9243  fin4en1  9566  ssfin4  9567  axdc3lem2  9708  axdc3lem4  9710  fpwwe2lem9  9895  recexsrlem  10360  nn0n0n1ge2b  11800  xmulpnf1  12506  ige2m2fzo  12938  swrdlsw  13853  swrd2lsw  14138  wrdl3s3  14148  lcmfass  15807  qredeu  15819  qnumdencoprm  15902  qeqnumdivden  15903  isacs1i  16745  subgga  18159  symgfixf1  18284  sylow1lem2  18442  sylow3lem1  18470  nn0gsumfz  18809  mptcoe1fsupp  20054  evls1gsumadd  20158  evls1gsummul  20159  evl1gsummul  20193  mat1scmat  20820  smadiadetlem4  20950  mptcoe1matfsupp  21082  chfacfscmulgsum  21140  chfacfpmmulgsum  21144  topbas  21252  neips  21393  lmbrf  21540  rnelfm  22233  tsmsres  22423  reconnlem1  23105  lmmbrf  23536  iscauf  23554  caucfil  23557  cmetcaulem  23562  voliunlem1  23822  isosctrlem1  25065  bcmono  25523  2lgslem1a  25637  dchrvmasumlem2  25744  mulog2sumlem2  25781  pntlemb  25843  usgr2pthlem  27219  2pthon3v  27397  elwspths2spth  27421  clwwlkccatlem  27442  clwlkclwwlklem2fv2  27449  clwwlkwwlksb  27508  grpofo  27955  nvss  28049  nmosetn0  28221  hhsst  28722  pjoc1i  28887  chlejb1i  28932  cmbr4i  29057  pjjsi  29156  nmopun  29470  stlesi  29697  mdsl2bi  29779  mdslmd1lem1  29781  xraddge02  30141  supxrnemnf  30154  qtopt1  30672  lmxrge0  30768  esumcst  30895  sigagenval  30972  measdivcstALTV  31057  oms0  31128  ballotlemfc0  31323  ballotlemfcc  31324  bnj945  31618  bnj986  31798  bnj1421  31884  fv1stcnv  32573  fv2ndcnv  32574  dftrpred3g  32626  frrlem11  32687  nodense  32750  nulssgt  32817  conway  32818  etasslt  32828  slerec  32831  fness  33251  nandsym1  33323  bj-finsumval0  34065  finixpnum  34354  poimirlem3  34372  poimirlem16  34385  poimirlem17  34386  poimirlem19  34388  poimirlem20  34389  poimirlem27  34396  ismblfin  34410  lcvexchlem5  35655  paddssat  36431  dibn0  37770  lclkrs2  38157  fiphp3d  38852  pellqrex  38912  jm2.16nn0  39037  rp-fakeanorass  39315  clsk1indlem2  39828  icccncfext  41665  wallispilem4  41849  fmtnorec1  43135  fmtnoprmfac1lem  43162  mod42tp1mod8  43203  stgoldbwt  43377  sbgoldbwt  43378  sbgoldbst  43379  evengpoap3  43400  wtgoldbnnsum4prm  43403  bgoldbnnsum3prm  43405  ply1mulgsumlem2  43875  ldepspr  43962  blennngt2o2  44087  inlinecirc02plem  44208
  Copyright terms: Public domain W3C validator