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  1023  trut  1547  equsv  2006  equsalv  2258  equsal  2415  2sb6rf  2471  sb4b  2473  sbequ8  2499  ralv  3470  ceqsal  3480  ceqsalv  3482  sbceqal  3808  relop  5811  acsfn0  17554  cmpsub  22788  ballotlemodife  33186  bj-equsvt  35320  bj-sbievw1  35387  bj-sbievw  35389  bj-ralvw  35422  wl-2mintru2  36035  wl-equsalvw  36070  wl-equsald  36071  lub0N  37724  glb0N  37728