Theorem a1bi 365

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  mt2bi  366  pm4.83  1021  trut  1543  equsv  2009  equsalv  2268  equsal  2439  2sb6rf  2497  sb4b  2499  sb4bOLD  2500  sbequ8  2543  ralv  3519  relop  5721  acsfn0  16931  cmpsub  22008  ballotlemodife  31755  bj-sbievw1  34169  bj-sbievw  34171  bj-ralvw  34198  wl-equsalvw  34793  wl-equsald  34794  lub0N  36340  glb0N  36344