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

Theorem jctl 527
 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 523 1 (𝜑 → (𝜓𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  mpanl1  699  mpanlr1  705  opeqsng  5380  relop  5708  odi  8201  endjudisj  9592  nn0n0n1ge2  11959  0mod  13274  expge1  13471  hashge2el2dif  13843  swrdccatin2  14091  swrd2lsw  14314  4dvdseven  15722  ndvdsp1  15760  istrkg2ld  26260  0wlkons1  27912  ococin  29197  cmbr4i  29390  iundifdif  30328  nepss  33008  axextndbi  33109  ontopbas  33836  bj-elccinfty  34577  ctbssinf  34771  poimirlem16  35021  mblfinlem4  35045  ismblfin  35046  fiphp3d  39680  eelT01  41341  eel0T1  41342  un01  41419  dirkercncf  42679  nnsum3primes4  44236  line2x  45098  line2y  45099
 Copyright terms: Public domain W3C validator