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 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  717  mpanr2  720  relopabi  5278  brprcneu  6222  mpt2eq12  6757  tfr3  7540  oaabslem  7768  omabslem  7771  isinf  8214  pssnn  8219  ige2m2fzo  12570  uzindi  12821  drsdirfi  16985  ga0  17777  lbsext  19211  lindfrn  20208  toprntopon  20777  fbssint  21689  filssufilg  21762  neiflim  21825  lmmbrf  23106  caucfil  23127  konigsbergssiedgwpr  27227  sspid  27708  onsucsuccmpi  32567  bj-restsn0  33163  bj-restn0  33168  poimirlem28  33567  lhpexle1  35612  diophun  37654  eldioph4b  37692  relexp1idm  38323  relexp0idm  38324  dvsid  38847  dvsef  38848  un10  39332  cnfex  39501  dvmptfprod  40478
  Copyright terms: Public domain W3C validator