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  2274  equsal  2421  2sb6rf  2477  sb4b  2479  sbequ8  2505  ralv  3467  ceqsal  3478  ceqsalv  3480  sbceqal  3802  relop  5799  acsfn0  17583  cmpsub  23344  ballotlemodife  34655  bj-equsvt  36980  bj-sbievw1  37046  bj-sbievw  37048  bj-ralvw  37080  wl-2mintru2  37696  wl-equsalvw  37743  wl-equsald  37744  wl-equsaldv  37745  lub0N  39449  glb0N  39453