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

Theorem jctr 524
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 520 1 (𝜑 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  mpanl2  701  mpanr2  704  exan  1861  relopabi  5831  brprcneu  6895  brprcneuALT  6896  mpoeq12  7507  tfr3  8440  oaabslem  8686  omabslem  8689  enrefnn  9088  pssnn  9209  isinf  9297  isinfOLD  9298  preleqALT  9658  ige2m2fzo  13768  uzindi  14024  drsdirfi  18352  ga0  19317  lbsext  21166  lindfrn  21842  toprntopon  22932  fbssint  23847  filssufilg  23920  neiflim  23983  lmmbrf  25297  caucfil  25318  lrrecfr  27977  konigsbergssiedgwpr  30269  sspid  30745  satfdmfmla  35406  satefvfmla1  35431  onsucsuccmpi  36445  bj-restn0  37092  poimirlem28  37656  lhpexle1  40011  diophun  42789  eldioph4b  42827  tfsconcatlem  43354  relexp1idm  43732  relexp0idm  43733  dvsid  44355  dvsef  44356  un10  44813  cnfex  45038  dvmptfprod  45965
  Copyright terms: Public domain W3C validator