MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jctl Structured version   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  |-  ps
Assertion
Ref Expression
jctl  |-  ( ph  ->  ( ps  /\  ph ) )

Proof of Theorem jctl
StepHypRef Expression
1 id 22 . 2  |-  ( ph  ->  ph )
2 jctl.1 . 2  |-  ps
31, 2jctil 537 1  |-  ( ph  ->  ( ps  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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
This theorem is referenced by:  mpanl1  680  mpanlr1  686  relop  5091  odi  7121  cdaun  8445  nn0n0n1ge2  10747  0mod  11849  expge1  12011  hashge2el2dif  12295  swrd2lsw  12663  ndvdsp1  13724  istrkg2ld  23048  cusgra3vnbpr  23518  constr2spthlem1  23638  2pthon  23646  constr3trllem2  23682  constr3pthlem1  23686  constr3pthlem2  23687  ococin  24956  cmbr4i  25149  iundifdif  26057  nepss  27511  axextndbi  27755  ontopbas  28411  mblfinlem4  28572  ismblfin  28573  fiphp3d  29299  wlkiswwlk2  30472  eelT01  31742  eel0T1  31743  un01  31825  bj-elccinfty  32846
  Copyright terms: Public domain W3C validator