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

Theorem jctl 525
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 19 . 2  |-  ( ph  ->  ph )
2 jctl.1 . 2  |-  ps
31, 2jctil 523 1  |-  ( ph  ->  ( ps  /\  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  mpanl1  661  mpanlr1  667  relop  4834  odi  6577  cdaun  7798  0mod  10995  expge1  11139  ndvdsp1  12608  ococin  21987  cmbr4i  22180  iundifdif  23160  prsiga  23492  nepss  24072  axextndbi  24161  ontopbas  24867  fiphp3d  26902  eelT01  28489  eel0T1  28490  un01  28564
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 177  df-an 360
  Copyright terms: Public domain W3C validator