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

Theorem jctl 562
 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 558 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 196  df-an 385 This theorem is referenced by:  mpanl1  712  mpanlr1  718  relop  5194  odi  7546  cdaun  8877  nn0n0n1ge2  11235  0mod  12563  expge1  12759  hashge2el2dif  13117  swrd2lsw  13543  4dvdseven  14947  ndvdsp1  14973  istrkg2ld  25159  cusgra3vnbpr  25994  constr2spthlem1  26124  2pthon  26132  constr3trllem2  26179  constr3pthlem1  26183  constr3pthlem2  26184  wlkiswwlk2  26225  ococin  27651  cmbr4i  27844  iundifdif  28763  nepss  30854  axextndbi  30954  ontopbas  31597  bj-elccinfty  32278  poimirlem16  32595  mblfinlem4  32619  ismblfin  32620  fiphp3d  36401  eelT01  37957  eel0T1  37958  un01  38037  dirkercncf  39000  nnsum3primes4  40204  wspthsnwspthsnon  41122  0wlkOns1  41289
 Copyright terms: Public domain W3C validator