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

Theorem jctl 526
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  |-  ps
Assertion
Ref Expression
jctl  |-  ( ph  ->  ( ps  /\  ph ) )

Proof of Theorem jctl
StepHypRef Expression
1 id 20 . 2  |-  ( ph  ->  ph )
2 jctl.1 . 2  |-  ps
31, 2jctil 524 1  |-  ( ph  ->  ( ps  /\  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpanl1  662  mpanlr1  668  relop  4956  odi  6751  cdaun  7978  nn0n0n1ge2  10205  0mod  11192  expge1  11337  ndvdsp1  12849  cusgra3vnbpr  21333  2pthon  21443  constr3trllem2  21479  constr3pthlem1  21483  constr3pthlem2  21484  ococin  22751  cmbr4i  22944  iundifdif  23850  nepss  24947  axextndbi  25178  ontopbas  25885  fiphp3d  26564  eelT01  28152  eel0T1  28153  un01  28235
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator