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  2422  2sb6rf  2478  sb4b  2480  sbequ8  2506  ralv  3457  ceqsal  3468  ceqsalv  3470  sbceqal  3791  relop  5807  acsfn0  17628  cmpsub  23367  ballotlemodife  34644  mh-infprim1bi  36730  mh-infprim2bi  36731  bj-equsvt  37070  bj-sbievw1  37154  bj-sbievw  37156  bj-ralvw  37188  wl-2mintru2  37809  wl-equsalvw  37865  wl-equsald  37866  wl-equsaldv  37867  lub0N  39637  glb0N  39641