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

Theorem jctl 563
 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 559 1 (𝜑 → (𝜓𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 197  df-an 385 This theorem is referenced by:  mpanl1  716  mpanlr1  722  relop  5305  odi  7704  cdaun  9032  nn0n0n1ge2  11396  0mod  12741  expge1  12937  hashge2el2dif  13300  swrd2lsw  13741  4dvdseven  15156  ndvdsp1  15182  istrkg2ld  25404  wspthsnwspthsnonOLD  26881  0wlkons1  27099  ococin  28395  cmbr4i  28588  iundifdif  29507  nepss  31725  axextndbi  31834  ontopbas  32552  bj-elccinfty  33231  poimirlem16  33555  mblfinlem4  33579  ismblfin  33580  fiphp3d  37700  eelT01  39253  eel0T1  39254  un01  39333  dirkercncf  40642  nnsum3primes4  42001
 Copyright terms: Public domain W3C validator