Theorem a1bi 213

Description: Inference rule introducing a theorem as an antecedent.

Hypothesis

Ref	Expression
a1bi.1	|- ph

Assertion

Ref	Expression
a1bi	|- (ps <-> (ph -> ps))

Proof of Theorem a1bi

Step	Hyp	Ref	Expression
1		ax-1 4	. 2 |- (ps -> (ph -> ps))
2		a1bi.1	. . 3 |- ph
3		pm2.27 76	. . 3 |- (ph -> ((ph -> ps) -> ps))
4	2, 3	ax-mp 7	. 2 |- ((ph -> ps) -> ps)
5	1, 4	impbii 173	1 |- (ps <-> (ph -> ps))

Syntax hints:   -> wi 3   <-> wb 162

This theorem is referenced by:  pm4.83 809  sbequ8 1456  a12lem1 1605  ralv 2138  hbsbc1vOLD 2298  eufromeq3 3641  relop 3924  pw2en 5316  caun0 9018  bnj28 12183  TFIid 13845  compsub 15113  glb0 16675

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 163

Copyright terms: Public domain