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

Theorem jctl 522
Description: Inference conjoining a theorem to the left of a consequent. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.)
Hypothesis
Ref Expression
jctl.1 𝜓
Assertion
Ref Expression
jctl (𝜑 → (𝜓𝜑))

Proof of Theorem jctl
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
2 jctl.1 . 2 𝜓
31, 2jctil 518 1 (𝜑 → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394
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 395
This theorem is referenced by:  mpanl1  698  mpanlr1  704  opeqsng  5501  relop  5849  odi  8601  ssfi  9204  endjudisj  10204  nn0n0n1ge2  12585  0mod  13916  expge1  14113  hashge2el2dif  14494  swrdccatin2  14732  swrd2lsw  14956  4dvdseven  16370  ndvdsp1  16408  istrkg2ld  28384  0wlkons1  30051  ococin  31338  cmbr4i  31531  iundifdif  32483  wevgblacfn  34949  nepss  35553  axextndbi  35641  ontopbas  36153  bj-elccinfty  36934  ctbssinf  37126  poimirlem16  37350  mblfinlem4  37374  ismblfin  37375  fiphp3d  42513  onmcl  43034  omabs2  43035  eelT01  44424  eel0T1  44425  un01  44502  dirkercncf  45764  nnsum3primes4  47396  vopnbgrelself  47458  line2x  48178  line2y  48179
  Copyright terms: Public domain W3C validator