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

Theorem jctr 566
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 562 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:  mpanl2  719  mpanr2  722  relopabi  5393  brprcneu  6337  mpt2eq12  6872  tfr3  7656  oaabslem  7884  omabslem  7887  isinf  8330  pssnn  8335  preleqALT  8677  ige2m2fzo  12717  uzindi  12967  drsdirfi  17131  ga0  17923  lbsext  19357  lindfrn  20354  toprntopon  20923  fbssint  21835  filssufilg  21908  neiflim  21971  lmmbrf  23252  caucfil  23273  konigsbergssiedgwpr  27393  sspid  27881  onsucsuccmpi  32740  bj-restsn0  33336  bj-restn0  33341  poimirlem28  33742  lhpexle1  35789  diophun  37831  eldioph4b  37869  relexp1idm  38500  relexp0idm  38501  dvsid  39024  dvsef  39025  un10  39509  cnfex  39678  dvmptfprod  40655
  Copyright terms: Public domain W3C validator