Theorem a1bi 363

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 361	. 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  364  pm4.83  1022  trut  1548  equsv  2010  equsalv  2263  equsal  2419  2sb6rf  2475  sb4b  2477  sb4bOLD  2478  sbequ8  2507  ralv  3455  sbceqal  3787  relop  5758  acsfn0  17367  cmpsub  22549  ballotlemodife  32460  bj-equsvt  34957  bj-sbievw1  35025  bj-sbievw  35027  bj-ralvw  35060  wl-2mintru2  35658  wl-equsalvw  35693  wl-equsald  35694  lub0N  37199  glb0N  37203