Theorem jctr 291

Description: Inference conjoining a theorem to the right of a consequent.

Hypothesis

Ref	Expression
jctr.1	|- ps

Assertion

Ref	Expression
jctr	|- (ph -> (ph /\ ps))

Proof of Theorem jctr

Step	Hyp	Ref	Expression
1		id 59	. 2 |- (ph -> ph)
2		jctr.1	. . 3 |- ps
3	2	a1i 8	. 2 |- (ph -> ps)
4	1, 3	jca 288	1 |- (ph -> (ph /\ ps))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  bm1.1 1462  tfr3 3926  oaabslem 4251  oaabs 4252  pssnn 4534  supeu 4578  ltpnft 5542  divdivmult 5795  subbasOLD 7644  retopbas 7655  neiint 7719  sspid 8384  hlimreu 9110  hlimeu 9111  pjpj0 9255

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain