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  3465  ceqsal  3476  ceqsalv  3478  sbceqal  3806  relop  5797  acsfn0  17584  cmpsub  23303  ballotlemodife  34465  bj-equsvt  36752  bj-sbievw1  36818  bj-sbievw  36820  bj-ralvw  36852  wl-2mintru2  37464  wl-equsalvw  37511  wl-equsald  37512  wl-equsaldv  37513  lub0N  39167  glb0N  39171