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  1042  trut  1576  equsv  2033  equsalv  2303  equsal  2449  2sb6rf  2505  sb4b  2507  sbequ8  2533  ralv  3481  ceqsal  3492  ceqsalv  3494  sbceqal  3805  relop  5836  acsfn0  17711  cmpsub  23557  ballotlemodife  34888  mh-infprim1bi  37057  mh-infprim2bi  37058  bj-equsvt  37396  bj-sbievw1  37480  bj-sbievw  37482  bj-ralvw  37514  wl-2mintru2  38137  wl-equsalvw  38193  wl-equsald  38194  wl-equsaldv  38195  lub0N  39963  glb0N  39967