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  1025  trut  1543  equsv  2002  equsalv  2268  equsal  2425  2sb6rf  2481  sb4b  2483  sbequ8  2509  ralv  3516  ceqsal  3527  ceqsalv  3529  sbceqal  3870  relop  5875  acsfn0  17718  cmpsub  23429  ballotlemodife  34462  bj-equsvt  36745  bj-sbievw1  36811  bj-sbievw  36813  bj-ralvw  36845  wl-2mintru2  37457  wl-equsalvw  37492  wl-equsald  37493  wl-equsaldv  37494  lub0N  39145  glb0N  39149