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 1455  tfr3 3911  oaabslem 4235  oaabs 4236  pssnn 4513  supeu 4552  ltpnft 5515  divdivmult 5751  subbas 7586  retopbas 7597  neiint 7660  sspid 8318  hlimreu 9031  hlimeu 9032  pjpj0 9170

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