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  5799  acsfn0  17617  cmpsub  23375  ballotlemodife  34658  mh-infprim1bi  36744  mh-infprim2bi  36745  bj-equsvt  37084  bj-sbievw1  37168  bj-sbievw  37170  bj-ralvw  37202  wl-2mintru2  37821  wl-equsalvw  37877  wl-equsald  37878  wl-equsaldv  37879  lub0N  39649  glb0N  39653