Theorem a1bi 366

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  mt2bi  367  pm4.83  1025  trut  1549  equsv  2012  equsalv  2266  equsal  2416  2sb6rf  2472  sb4b  2474  sb4bOLD  2475  sbequ8  2504  ralv  3422  relop  5704  acsfn0  17117  cmpsub  22251  ballotlemodife  32130  bj-equsvt  34647  bj-sbievw1  34715  bj-sbievw  34717  bj-ralvw  34751  wl-2mintru2  35348  wl-equsalvw  35383  wl-equsald  35384  lub0N  36889  glb0N  36893