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

Theorem jctl 541
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 537 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  mpanl1  680  mpanlr1  686  relop  5158  odi  7247  cdaun  8573  nn0n0n1ge2  10884  0mod  12027  expge1  12203  hashge2el2dif  12521  swrd2lsw  12890  ndvdsp1  14067  istrkg2ld  23858  cusgra3vnbpr  24465  constr2spthlem1  24596  2pthon  24604  constr3trllem2  24651  constr3pthlem1  24655  constr3pthlem2  24656  wlkiswwlk2  24697  ococin  26326  cmbr4i  26519  iundifdif  27430  nepss  29095  axextndbi  29237  ontopbas  29893  mblfinlem4  30054  ismblfin  30055  fiphp3d  30753  dirkercncf  31889  eelT01  33503  eel0T1  33504  un01  33586  bj-elccinfty  34617
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 185  df-an 371
  Copyright terms: Public domain W3C validator