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  2272  equsal  2419  2sb6rf  2475  sb4b  2477  sbequ8  2503  ralv  3464  ceqsal  3475  ceqsalv  3477  sbceqal  3799  relop  5796  acsfn0  17570  cmpsub  23318  ballotlemodife  34534  bj-equsvt  36846  bj-sbievw1  36912  bj-sbievw  36914  bj-ralvw  36946  wl-2mintru2  37558  wl-equsalvw  37605  wl-equsald  37606  wl-equsaldv  37607  lub0N  39311  glb0N  39315