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  4850  odi  6593  cdaun  7814  0mod  11011  expge1  11155  ndvdsp1  12624  ococin  22003  cmbr4i  22196  iundifdif  23176  prsiga  23507  nepss  24087  axextndbi  24232  ontopbas  24939  fiphp3d  27005  cusgra3vnbpr  28300  constr3trllem2  28397  constr3pthlem1  28401  constr3pthlem2  28402  eelT01  28795  eel0T1  28796  un01  28878
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