Theorem jctl 564

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

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( ph -> ph )
2		jctl.1	. 2 |- ps
3	1, 2	jctil 560	1 |- ( ph -> ( ps /\ ph ) )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  mpanl1  716  mpanlr1  722  relop  5272  odi  7659  cdaun  8994  nn0n0n1ge2  11358  0mod  12701  expge1  12897  hashge2el2dif  13262  swrd2lsw  13695  4dvdseven  15109  ndvdsp1  15135  istrkg2ld  25359  wspthsnwspthsnon  26811  0wlkons1  26982  ococin  28267  cmbr4i  28460  iundifdif  29381  nepss  31599  axextndbi  31710  ontopbas  32427  bj-elccinfty  33101  poimirlem16  33425  mblfinlem4  33449  ismblfin  33450  fiphp3d  37383  eelT01  38936  eel0T1  38937  un01  39016  dirkercncf  40324  nnsum3primes4  41676