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

Theorem jctr 521
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 517 1 (𝜑 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385
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 199  df-an 386
This theorem is referenced by:  mpanl2  693  mpanr2  696  exan  1958  relopabi  5449  brprcneu  6403  mpt2eq12  6949  tfr3  7734  oaabslem  7963  omabslem  7966  isinf  8415  pssnn  8420  preleqALT  8762  ige2m2fzo  12786  uzindi  13036  drsdirfi  17253  ga0  18043  lbsext  19486  lindfrn  20485  toprntopon  21058  fbssint  21970  filssufilg  22043  neiflim  22106  lmmbrf  23388  caucfil  23409  konigsbergssiedgwpr  27596  sspid  28105  onsucsuccmpi  32950  bj-restsn0  33531  bj-restn0  33536  poimirlem28  33926  lhpexle1  36029  diophun  38123  eldioph4b  38161  relexp1idm  38789  relexp0idm  38790  dvsid  39312  dvsef  39313  un10  39784  cnfex  39947  dvmptfprod  40904
  Copyright terms: Public domain W3C validator