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

Theorem jctir 560
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 553 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  jctr  564  uniintsn  4546  ordunidif  5811  funtp  5983  foimacnv  6192  respreima  6384  fpr  6461  curry1  7314  dmtpos  7409  wfrlem13  7472  oawordeulem  7679  oelim2  7720  oaabs2  7770  ixpsnf1o  7990  ssdomg  8043  fodomr  8152  limenpsi  8176  cantnfrescl  8611  cardprclem  8843  fin4en1  9169  ssfin4  9170  axdc3lem2  9311  axdc3lem4  9313  fpwwe2lem9  9498  reclem2pr  9908  recexsrlem  9962  nn0n0n1ge2b  11397  xmulpnf1  12142  ige2m2fzo  12570  swrdlsw  13498  swrd2lsw  13741  wrdl3s3  13751  climeu  14330  algcvgblem  15337  lcmfass  15406  qredeu  15419  qnumdencoprm  15500  qeqnumdivden  15501  isacs1i  16365  subgga  17779  symgfixf1  17903  sylow1lem2  18060  sylow3lem1  18088  nn0gsumfz  18426  mptcoe1fsupp  19633  evls1gsumadd  19737  evls1gsummul  19738  evl1gsummul  19772  mat1scmat  20393  smadiadetlem4  20523  mptcoe1matfsupp  20655  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  eltg3i  20813  topbas  20824  neips  20965  lmbrf  21112  rnelfm  21804  tsmsres  21994  reconnlem1  22676  lmmbrf  23106  iscauf  23124  caucfil  23127  cmetcaulem  23132  voliunlem1  23364  isosctrlem1  24593  bcmono  25047  2lgslem1a  25161  dchrvmasumlem2  25232  mulog2sumlem2  25269  pntlemb  25331  axlowdimlem13  25879  usgr2pthlem  26715  2pthon3v  26908  elwspths2spth  26934  clwlkclwwlklem2fv2  26962  clwlksf1clwwlk  27056  clwwlkccatlem  27331  grpofo  27481  nvss  27576  nmosetn0  27748  hhsst  28251  pjoc1i  28418  chlejb1i  28463  cmbr4i  28588  pjjsi  28687  nmopun  29001  stlesi  29228  mdsl2bi  29310  mdslmd1lem1  29312  xraddge02  29649  supxrnemnf  29662  qtopt1  30030  lmxrge0  30126  esumcst  30253  sigagenval  30331  measdivcstOLD  30415  oms0  30487  ballotlemfc0  30682  ballotlemfcc  30683  bnj945  30970  bnj150  31072  bnj986  31150  bnj1421  31236  dftrpred3g  31857  nodense  31967  nulssgt  32034  conway  32035  etasslt  32045  slerec  32048  fness  32469  nandsym1  32546  bj-finsumval0  33277  finixpnum  33524  poimirlem3  33542  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem27  33566  ismblfin  33580  rngoideu  33832  lcvexchlem5  34643  paddssat  35418  dibn0  36759  lclkrs2  37146  fiphp3d  37700  pellqrex  37760  jm2.16nn0  37888  rp-fakeanorass  38175  clsk1indlem2  38657  icccncfext  40418  wallispilem4  40603  fmtnorec1  41774  fmtnoprmfac1lem  41801  mod42tp1mod8  41844  stgoldbwt  41989  sbgoldbwt  41990  sbgoldbst  41991  evengpoap3  42012  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017  ply1mulgsumlem2  42500  ldepspr  42587  blennngt2o2  42711
  Copyright terms: Public domain W3C validator