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

Theorem jctir 522
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 513 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  jctr  526  ordunidif  6367  funtp  6559  dmtpos  8170  frrlem11  8228  oaabs2  8596  ixpsnf1o  8879  fodomr  9075  mapfienlem2  9347  cantnfrescl  9617  dfttrcl2  9665  cardprclem  9920  fin4en1  10250  ssfin4  10251  axdc3lem2  10392  axdc3lem4  10394  fpwwe2lem8  10579  recexsrlem  11044  nn0n0n1ge2b  12486  xmulpnf1  13199  ige2m2fzo  13641  swrdlsw  14561  swrd2lsw  14847  wrdl3s3  14857  lcmfass  16527  qredeu  16539  qnumdencoprm  16625  qeqnumdivden  16626  isacs1i  17542  subgga  19085  symgfixf1  19224  sylow1lem2  19386  sylow3lem1  19414  nn0gsumfz  19766  evlsgsumadd  21517  evlsgsummul  21518  mhpmulcl  21555  mptcoe1fsupp  21602  evls1gsumadd  21706  evls1gsummul  21707  evl1gsummul  21742  mat1scmat  21904  smadiadetlem4  22034  mptcoe1matfsupp  22167  chfacfscmulgsum  22225  chfacfpmmulgsum  22229  topbas  22338  neips  22480  lmbrf  22627  rnelfm  23320  tsmsres  23511  reconnlem1  24205  lmmbrf  24642  iscauf  24660  caucfil  24663  cmetcaulem  24668  voliunlem1  24930  isosctrlem1  26184  bcmono  26641  2lgslem1a  26755  dchrvmasumlem2  26862  mulog2sumlem2  26899  pntlemb  26961  nodense  27056  conway  27160  etasslt  27174  slerec  27180  cofcutr  27265  usgr2pthlem  28753  2pthon3v  28930  elwspths2spth  28954  clwlkclwwlklem2fv2  28982  grpofo  29483  nvss  29577  nmosetn0  29749  hhsst  30250  pjoc1i  30415  chlejb1i  30460  cmbr4i  30585  pjjsi  30684  nmopun  30998  stlesi  31225  mdsl2bi  31307  mdslmd1lem1  31309  xraddge02  31708  supxrnemnf  31720  qtopt1  32473  lmxrge0  32590  esumcst  32719  sigagenval  32796  measdivcstALTV  32881  oms0  32954  ballotlemfc0  33149  ballotlemfcc  33150  bnj945  33442  bnj986  33624  bnj1421  33711  fv1stcnv  34407  fv2ndcnv  34408  fness  34867  nandsym1  34940  bj-finsumval0  35802  finixpnum  36109  poimirlem3  36127  poimirlem16  36140  poimirlem17  36141  poimirlem19  36143  poimirlem20  36144  poimirlem27  36151  ismblfin  36165  lcvexchlem5  37546  paddssat  38323  dibn0  39662  lclkrs2  40049  aks4d1p1p7  40577  fiphp3d  41185  pellqrex  41245  jm2.16nn0  41371  onexlimgt  41620  cantnf2  41703  rp-fakeanorass  41873  clsk1indlem2  42402  icccncfext  44214  wallispilem4  44395  fmtnorec1  45815  fmtnoprmfac1lem  45842  mod42tp1mod8  45880  stgoldbwt  46054  sbgoldbwt  46055  sbgoldbst  46056  evengpoap3  46077  wtgoldbnnsum4prm  46080  bgoldbnnsum3prm  46082  ply1mulgsumlem2  46554  ldepspr  46640  blennngt2o2  46764  inlinecirc02plem  46958
  Copyright terms: Public domain W3C validator