Theorem a1bi 362

Description: Inference introducing a theorem as an antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)

Hypothesis

Ref	Expression
a1bi.1	⊢ 𝜑

Assertion

Ref	Expression
a1bi	⊢ (𝜓 ↔ (𝜑 → 𝜓))

Proof of Theorem a1bi

Step	Hyp	Ref	Expression
1		a1bi.1	. 2 ⊢ 𝜑
2		biimt 360	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  mt2bi  363  pm4.83  1026  trut  1546  equsv  2003  equsalv  2268  equsal  2422  2sb6rf  2478  sb4b  2480  sbequ8  2506  ralv  3492  ceqsal  3503  ceqsalv  3505  sbceqal  3832  relop  5835  acsfn0  17677  cmpsub  23343  ballotlemodife  34535  bj-equsvt  36802  bj-sbievw1  36868  bj-sbievw  36870  bj-ralvw  36902  wl-2mintru2  37514  wl-equsalvw  37561  wl-equsald  37562  wl-equsaldv  37563  lub0N  39212  glb0N  39216