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

Theorem jctr 564
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 560 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:  mpanl2  716  mpanr2  719  relopabi  5215  brprcneu  6151  mpt2eq12  6680  tfr3  7455  oaabslem  7683  omabslem  7686  isinf  8133  pssnn  8138  ige2m2fzo  12487  uzindi  12737  drsdirfi  16878  ga0  17671  lbsext  19103  lindfrn  20100  toprntopon  20669  fbssint  21582  filssufilg  21655  neiflim  21718  lmmbrf  23000  caucfil  23021  konigsbergssiedgwpr  27010  sspid  27468  onsucsuccmpi  32137  bj-restsn0  32728  bj-restn0  32733  poimirlem28  33108  lhpexle1  34813  diophun  36856  eldioph4b  36894  relexp1idm  37526  relexp0idm  37527  dvsid  38051  dvsef  38052  un10  38536  cnfex  38709  dvmptfprod  39497
  Copyright terms: Public domain W3C validator