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 208  df-an 397
This theorem is referenced by:  mpanl2  697  mpanr2  700  exan  1855  exanOLD  1856  relopabi  5692  brprcneu  6658  mpoeq12  7222  tfr3  8029  oaabslem  8263  omabslem  8266  isinf  8723  pssnn  8728  preleqALT  9072  ige2m2fzo  13093  uzindi  13343  drsdirfi  17540  ga0  18360  lbsext  19857  lindfrn  20883  toprntopon  21451  fbssint  22364  filssufilg  22437  neiflim  22500  lmmbrf  23782  caucfil  23803  konigsbergssiedgwpr  27944  sspid  28418  satfdmfmla  32533  satefvfmla1  32558  onsucsuccmpi  33677  bj-restn0  34264  poimirlem28  34789  lhpexle1  37013  diophun  39237  eldioph4b  39275  relexp1idm  39926  relexp0idm  39927  dvsid  40530  dvsef  40531  un10  40989  cnfex  41152  dvmptfprod  42097
  Copyright terms: Public domain W3C validator