MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jctl Structured version   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  equvini  2079  relop  5015  odi  6814  cdaun  8044  nn0n0n1ge2  10272  0mod  11264  expge1  11409  ndvdsp1  12921  cusgra3vnbpr  21466  constr2spthlem1  21586  2pthon  21594  constr3trllem2  21630  constr3pthlem1  21634  constr3pthlem2  21635  ococin  22902  cmbr4i  23095  iundifdif  24005  nepss  25167  axextndbi  25424  ontopbas  26170  mblfinlem3  26236  ismblfin  26237  fiphp3d  26871  eelT01  28755  eel0T1  28756  un01  28838
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