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  1548  equsv  2005  equsalv  2275  equsal  2422  2sb6rf  2478  sb4b  2480  sbequ8  2506  ralv  3469  ceqsal  3480  ceqsalv  3482  sbceqal  3804  relop  5807  acsfn0  17595  cmpsub  23356  ballotlemodife  34676  bj-equsvt  37014  bj-sbievw1  37093  bj-sbievw  37095  bj-ralvw  37127  wl-2mintru2  37746  wl-equsalvw  37793  wl-equsald  37794  wl-equsaldv  37795  lub0N  39565  glb0N  39569