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  1026  trut  1547  equsv  2004  equsalv  2270  equsal  2417  2sb6rf  2473  sb4b  2475  sbequ8  2501  ralv  3463  ceqsal  3474  ceqsalv  3476  sbceqal  3803  relop  5790  acsfn0  17566  cmpsub  23316  ballotlemodife  34509  bj-equsvt  36819  bj-sbievw1  36885  bj-sbievw  36887  bj-ralvw  36919  wl-2mintru2  37531  wl-equsalvw  37578  wl-equsald  37579  wl-equsaldv  37580  lub0N  39234  glb0N  39238