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

Theorem jctl 543
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 539 1  |-  ( ph  ->  ( ps  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  mpanl1  684  mpanlr1  690  relop  4947  odi  7235  cdaun  8553  nn0n0n1ge2  10883  0mod  12078  expge1  12259  hashge2el2dif  12585  swrd2lsw  12971  ndvdsp1  14333  istrkg2ld  24450  cusgra3vnbpr  25135  constr2spthlem1  25266  2pthon  25274  constr3trllem2  25321  constr3pthlem1  25325  constr3pthlem2  25326  wlkiswwlk2  25367  ococin  27003  cmbr4i  27196  iundifdif  28124  nepss  30302  axextndbi  30402  ontopbas  31037  bj-elccinfty  31563  poimirlem16  31863  mblfinlem4  31887  ismblfin  31888  fiphp3d  35574  eelT01  37010  eel0T1  37011  un01  37092  dirkercncf  37852  nnsum3primes4  38696
  Copyright terms: Public domain W3C validator