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  2415  2sb6rf  2471  sb4b  2473  sbequ8  2499  ralv  3474  ceqsal  3485  ceqsalv  3487  sbceqal  3815  relop  5814  acsfn0  17621  cmpsub  23287  ballotlemodife  34489  bj-equsvt  36767  bj-sbievw1  36833  bj-sbievw  36835  bj-ralvw  36867  wl-2mintru2  37479  wl-equsalvw  37526  wl-equsald  37527  wl-equsaldv  37528  lub0N  39182  glb0N  39186