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  1027  trut  1546  equsv  2002  equsalv  2267  equsal  2422  2sb6rf  2478  sb4b  2480  sbequ8  2506  ralv  3508  ceqsal  3519  ceqsalv  3521  sbceqal  3851  relop  5861  acsfn0  17703  cmpsub  23408  ballotlemodife  34500  bj-equsvt  36780  bj-sbievw1  36846  bj-sbievw  36848  bj-ralvw  36880  wl-2mintru2  37492  wl-equsalvw  37539  wl-equsald  37540  wl-equsaldv  37541  lub0N  39190  glb0N  39194