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

Theorem jctl 539
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 535 1  |-  ( ph  ->  ( ps  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  mpanl1  678  mpanlr1  684  relop  5142  odi  7220  cdaun  8543  nn0n0n1ge2  10855  0mod  12010  expge1  12188  hashge2el2dif  12508  swrd2lsw  12884  ndvdsp1  14154  istrkg2ld  24059  cusgra3vnbpr  24670  constr2spthlem1  24801  2pthon  24809  constr3trllem2  24856  constr3pthlem1  24860  constr3pthlem2  24861  wlkiswwlk2  24902  ococin  26527  cmbr4i  26720  iundifdif  27643  nepss  29339  axextndbi  29480  ontopbas  30124  mblfinlem4  30297  ismblfin  30298  fiphp3d  30995  dirkercncf  32131  eelT01  33916  eel0T1  33917  un01  33999  bj-elccinfty  35036
  Copyright terms: Public domain W3C validator