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

Theorem jctl 550
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 546 1  |-  ( ph  ->  ( ps  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  mpanl1  694  mpanlr1  700  relop  4990  odi  7298  cdaun  8620  nn0n0n1ge2  10956  0mod  12161  expge1  12347  hashge2el2dif  12678  swrd2lsw  13102  ndvdsp1  14469  istrkg2ld  24587  cusgra3vnbpr  25272  constr2spthlem1  25403  2pthon  25411  constr3trllem2  25458  constr3pthlem1  25462  constr3pthlem2  25463  wlkiswwlk2  25504  ococin  27142  cmbr4i  27335  iundifdif  28255  nepss  30422  axextndbi  30522  ontopbas  31159  bj-elccinfty  31726  poimirlem16  32020  mblfinlem4  32044  ismblfin  32045  fiphp3d  35733  eelT01  37159  eel0T1  37160  un01  37239  dirkercncf  38081  nnsum3primes4  39028
  Copyright terms: Public domain W3C validator