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  1024  trut  1548  equsv  2007  equsalv  2259  equsal  2417  2sb6rf  2473  sb4b  2475  sbequ8  2501  ralv  3499  ceqsal  3510  ceqsalv  3512  sbceqal  3844  relop  5851  acsfn0  17604  cmpsub  22904  ballotlemodife  33496  bj-equsvt  35657  bj-sbievw1  35724  bj-sbievw  35726  bj-ralvw  35759  wl-2mintru2  36372  wl-equsalvw  36407  wl-equsald  36408  lub0N  38059  glb0N  38063