Theorem a1bi 365

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 363	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  mt2bi  366  pm4.83  1040  trut  1573  equsv  2030  equsalv  2309  equsal  2455  2sb6rf  2511  sb4b  2513  sbequ8  2539  ralv  3489  ceqsal  3500  ceqsalv  3502  sbceqal  3814  relop  5837  acsfn0  17715  cmpsub  23525  ballotlemodife  34832  mh-infprim1bi  36945  mh-infprim2bi  36946  bj-equsvt  37284  bj-sbievw1  37368  bj-sbievw  37370  bj-ralvw  37402  wl-2mintru2  38024  wl-equsalvw  38080  wl-equsald  38081  wl-equsaldv  38082  lub0N  39852  glb0N  39856