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

Theorem jctr 525
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 521 1 (𝜑 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 397
This theorem is referenced by:  mpanl2  699  mpanr2  702  exan  1865  relopabi  5776  brprcneu  6829  brprcneuALT  6830  mpoeq12  7424  tfr3  8337  oaabslem  8585  omabslem  8588  enrefnn  8949  pssnn  9070  isinf  9162  isinfOLD  9163  pssnnOLD  9167  preleqALT  9511  ige2m2fzo  13589  uzindi  13841  drsdirfi  18153  ga0  19036  lbsext  20576  lindfrn  21179  toprntopon  22225  fbssint  23140  filssufilg  23213  neiflim  23276  lmmbrf  24577  caucfil  24598  konigsbergssiedgwpr  29021  sspid  29495  satfdmfmla  33797  satefvfmla1  33822  lrrecfr  34251  onsucsuccmpi  34846  bj-restn0  35492  poimirlem28  36037  lhpexle1  38402  diophun  40998  eldioph4b  41036  relexp1idm  41890  relexp0idm  41891  dvsid  42515  dvsef  42516  un10  42974  cnfex  43137  dvmptfprod  44080
  Copyright terms: Public domain W3C validator