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

Theorem jctir 524
 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 515 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  jctr  528  ordunidif  6217  funtp  6390  dmtpos  7891  oaabs2  8259  ixpsnf1o  8489  fodomr  8656  mapfienlem2  8857  cantnfrescl  9127  cardprclem  9396  fin4en1  9720  ssfin4  9721  axdc3lem2  9862  axdc3lem4  9864  fpwwe2lem9  10049  recexsrlem  10514  nn0n0n1ge2b  11951  xmulpnf1  12655  ige2m2fzo  13095  swrdlsw  14020  swrd2lsw  14305  wrdl3s3  14317  lcmfass  15979  qredeu  15991  qnumdencoprm  16074  qeqnumdivden  16075  isacs1i  16919  subgga  18421  symgfixf1  18556  sylow1lem2  18715  sylow3lem1  18743  nn0gsumfz  19095  evlsgsumadd  20761  evlsgsummul  20762  mptcoe1fsupp  20842  evls1gsumadd  20946  evls1gsummul  20947  evl1gsummul  20982  mat1scmat  21142  smadiadetlem4  21272  mptcoe1matfsupp  21405  chfacfscmulgsum  21463  chfacfpmmulgsum  21467  topbas  21575  neips  21716  lmbrf  21863  rnelfm  22556  tsmsres  22747  reconnlem1  23429  lmmbrf  23864  iscauf  23882  caucfil  23885  cmetcaulem  23890  voliunlem1  24152  isosctrlem1  25402  bcmono  25859  2lgslem1a  25973  dchrvmasumlem2  26080  mulog2sumlem2  26117  pntlemb  26179  usgr2pthlem  27550  2pthon3v  27727  elwspths2spth  27751  clwlkclwwlklem2fv2  27779  grpofo  28280  nvss  28374  nmosetn0  28546  hhsst  29047  pjoc1i  29212  chlejb1i  29257  cmbr4i  29382  pjjsi  29481  nmopun  29795  stlesi  30022  mdsl2bi  30104  mdslmd1lem1  30106  xraddge02  30490  supxrnemnf  30503  qtopt1  31157  lmxrge0  31269  esumcst  31396  sigagenval  31473  measdivcstALTV  31558  oms0  31629  ballotlemfc0  31824  ballotlemfcc  31825  bnj945  32119  bnj986  32301  bnj1421  32388  fv1stcnv  33094  fv2ndcnv  33095  dftrpred3g  33146  frrlem11  33207  nodense  33270  nulssgt  33337  conway  33338  etasslt  33348  slerec  33351  fness  33771  nandsym1  33844  bj-finsumval0  34661  finixpnum  35001  poimirlem3  35019  poimirlem16  35032  poimirlem17  35033  poimirlem19  35035  poimirlem20  35036  poimirlem27  35043  ismblfin  35057  lcvexchlem5  36293  paddssat  37069  dibn0  38408  lclkrs2  38795  fiphp3d  39691  pellqrex  39751  jm2.16nn0  39876  rp-fakeanorass  40152  clsk1indlem2  40679  icccncfext  42469  wallispilem4  42650  fmtnorec1  43994  fmtnoprmfac1lem  44021  mod42tp1mod8  44060  stgoldbwt  44234  sbgoldbwt  44235  sbgoldbst  44236  evengpoap3  44257  wtgoldbnnsum4prm  44260  bgoldbnnsum3prm  44262  ply1mulgsumlem2  44735  ldepspr  44822  blennngt2o2  44946  inlinecirc02plem  45140
 Copyright terms: Public domain W3C validator