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

Theorem jctr 563
 Description: Inference conjoining a theorem to the right of a consequent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.)
Hypothesis
Ref Expression
jctl.1 𝜓
Assertion
Ref Expression
jctr (𝜑 → (𝜑𝜓))

Proof of Theorem jctr
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
2 jctl.1 . 2 𝜓
31, 2jctir 559 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 196  df-an 385 This theorem is referenced by:  mpanl2  713  mpanr2  716  relopabi  5167  brprcneu  6096  mpt2eq12  6613  tfr3  7382  oaabslem  7610  omabslem  7613  isinf  8058  pssnn  8063  ige2m2fzo  12398  uzindi  12643  drsdirfi  16761  ga0  17554  lbsext  18984  lindfrn  19979  fbssint  21452  filssufilg  21525  neiflim  21588  lmmbrf  22868  caucfil  22889  constr2spth  26130  constr2pth  26131  constr3lem4  26175  sspid  26964  onsucsuccmpi  31612  bj-restsn0  32219  bj-restn0  32224  bj-toprntopon  32244  poimirlem28  32607  lhpexle1  34312  diophun  36355  eldioph4b  36393  relexp1idm  37025  relexp0idm  37026  dvsid  37552  dvsef  37553  un10  38036  cnfex  38210  dvmptfprod  38835  konigsbergssiedgwpr  41418
 Copyright terms: Public domain W3C validator