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

Theorem jctr 528
 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 524 1 (𝜑 → (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  mpanl2  700  mpanr2  703  exan  1863  relopabi  5659  brprcneu  6638  mpoeq12  7207  tfr3  8021  oaabslem  8256  omabslem  8259  isinf  8718  pssnn  8723  preleqALT  9067  ige2m2fzo  13098  uzindi  13348  drsdirfi  17543  ga0  18424  lbsext  19932  lindfrn  20515  toprntopon  21540  fbssint  22453  filssufilg  22526  neiflim  22589  lmmbrf  23876  caucfil  23897  konigsbergssiedgwpr  28044  sspid  28518  satfdmfmla  32775  satefvfmla1  32800  onsucsuccmpi  33919  bj-restn0  34524  poimirlem28  35104  lhpexle1  37323  diophun  39757  eldioph4b  39795  relexp1idm  40458  relexp0idm  40459  dvsid  41078  dvsef  41079  un10  41537  cnfex  41700  dvmptfprod  42630
 Copyright terms: Public domain W3C validator