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

Theorem jctr 526
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 522 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:  mpanl2  700  mpanr2  703  exan  1866  relopabi  5782  brprcneu  6836  brprcneuALT  6837  mpoeq12  7434  tfr3  8349  oaabslem  8597  omabslem  8600  enrefnn  8997  pssnn  9118  isinf  9210  isinfOLD  9211  pssnnOLD  9215  preleqALT  9561  ige2m2fzo  13644  uzindi  13896  drsdirfi  18202  ga0  19086  lbsext  20669  lindfrn  21250  toprntopon  22297  fbssint  23212  filssufilg  23285  neiflim  23348  lmmbrf  24649  caucfil  24670  lrrecfr  27284  konigsbergssiedgwpr  29242  sspid  29716  satfdmfmla  34058  satefvfmla1  34083  onsucsuccmpi  34968  bj-restn0  35611  poimirlem28  36156  lhpexle1  38521  diophun  41143  eldioph4b  41181  relexp1idm  42078  relexp0idm  42079  dvsid  42703  dvsef  42704  un10  43162  cnfex  43325  dvmptfprod  44276
  Copyright terms: Public domain W3C validator