Theorem a1bi 363

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 361	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  mt2bi  364  pm4.83  1022  trut  1545  equsv  2006  equsalv  2259  equsal  2417  2sb6rf  2473  sb4b  2475  sb4bOLD  2476  sbequ8  2505  ralv  3456  sbceqal  3782  relop  5759  acsfn0  17369  cmpsub  22551  ballotlemodife  32464  bj-equsvt  34961  bj-sbievw1  35029  bj-sbievw  35031  bj-ralvw  35064  wl-2mintru2  35662  wl-equsalvw  35697  wl-equsald  35698  lub0N  37203  glb0N  37207