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  1027  trut  1548  equsv  2005  equsalv  2275  equsal  2421  2sb6rf  2477  sb4b  2479  sbequ8  2505  ralv  3456  ceqsal  3467  ceqsalv  3469  sbceqal  3790  relop  5805  acsfn0  17626  cmpsub  23365  ballotlemodife  34642  mh-infprim1bi  36728  mh-infprim2bi  36729  bj-equsvt  37068  bj-sbievw1  37152  bj-sbievw  37154  bj-ralvw  37186  wl-2mintru2  37807  wl-equsalvw  37863  wl-equsald  37864  wl-equsaldv  37865  lub0N  39635  glb0N  39639