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 554 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  jctr  564  uniintsn  4484  ordunidif  5737  funtp  5908  foimacnv  6116  respreima  6305  fpr  6381  curry1  7221  dmtpos  7316  wfrlem13  7379  oawordeulem  7586  oelim2  7627  oaabs2  7677  ixpsnf1o  7900  ssdomg  7953  fodomr  8063  limenpsi  8087  cantnfrescl  8525  cardprclem  8757  fin4en1  9083  ssfin4  9084  axdc3lem2  9225  axdc3lem4  9227  fpwwe2lem9  9412  reclem2pr  9822  recexsrlem  9876  nn0n0n1ge2b  11311  xmulpnf1  12055  ige2m2fzo  12479  swrdlsw  13398  swrd2lsw  13637  wrdl3s3  13647  climeu  14228  algcvgblem  15225  lcmfass  15294  qredeu  15307  qnumdencoprm  15388  qeqnumdivden  15389  isacs1i  16250  subgga  17665  symgfixf1  17789  sylow1lem2  17946  sylow3lem1  17974  nn0gsumfz  18312  mptcoe1fsupp  19517  evls1gsumadd  19621  evls1gsummul  19622  evl1gsummul  19656  mat1scmat  20277  smadiadetlem4  20407  mptcoe1matfsupp  20539  chfacfscmulgsum  20597  chfacfpmmulgsum  20601  eltg3i  20689  topbas  20700  neips  20840  lmbrf  20987  rnelfm  21680  tsmsres  21870  reconnlem1  22552  lmmbrf  22983  iscauf  23001  caucfil  23004  cmetcaulem  23009  voliunlem1  23241  isosctrlem1  24465  bcmono  24919  2lgslem1a  25033  dchrvmasumlem2  25104  mulog2sumlem2  25141  pntlemb  25203  axlowdimlem13  25751  usgr2pthlem  26545  2pthon3v  26725  elwspths2spth  26746  clwlkclwwlklem2fv2  26781  clwlksf1clwwlk  26852  frgrhash2wsp  27072  grpofo  27223  nvss  27318  nmosetn0  27490  hhsst  27993  pjoc1i  28160  chlejb1i  28205  cmbr4i  28330  pjjsi  28429  nmopun  28743  stlesi  28970  mdsl2bi  29052  mdslmd1lem1  29054  xraddge02  29388  supxrnemnf  29401  qtopt1  29708  lmxrge0  29804  esumcst  29930  sigagenval  30008  measdivcstOLD  30092  oms0  30164  ballotlemfc0  30359  ballotlemfcc  30360  bnj945  30587  bnj150  30689  bnj986  30767  bnj1421  30853  dftrpred3g  31469  nodense  31587  fness  32021  nandsym1  32098  bj-finsumval0  32815  finixpnum  33061  poimirlem3  33079  poimirlem16  33092  poimirlem17  33093  poimirlem19  33095  poimirlem20  33096  poimirlem27  33103  ismblfin  33117  rngoideu  33369  lcvexchlem5  33840  paddssat  34615  dibn0  35957  lclkrs2  36344  fiphp3d  36898  pellqrex  36958  jm2.16nn0  37086  rp-fakeanorass  37374  clsk1indlem2  37857  icccncfext  39431  wallispilem4  39618  fmtnorec1  40774  fmtnoprmfac1lem  40801  mod42tp1mod8  40844  stgoldbwt  40985  bgoldbwt  40986  bgoldbst  40987  evengpoap3  41002  wtgoldbnnsum4prm  41005  bgoldbnnsum3prm  41007  ply1mulgsumlem2  41489  ldepspr  41576  blennngt2o2  41704
  Copyright terms: Public domain W3C validator