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 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  363  pm4.83  1021  trut  1545  equsv  2007  equsalv  2262  equsal  2417  2sb6rf  2473  sb4b  2475  sb4bOLD  2476  sbequ8  2505  ralv  3446  sbceqal  3778  relop  5748  acsfn0  17286  cmpsub  22459  ballotlemodife  32364  bj-equsvt  34888  bj-sbievw1  34956  bj-sbievw  34958  bj-ralvw  34991  wl-2mintru2  35589  wl-equsalvw  35624  wl-equsald  35625  lub0N  37130  glb0N  37134