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 ⊢ (𝜓 ↔ (𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  mt2bi  366  pm4.83  1042  trut  1575  equsv  2035  equsalv  2301  equsal  2446  2sb6rf  2502  sb4b  2504  sbequ8  2530  ralv  3476  ceqsal  3487  ceqsalv  3489  sbceqal  3799  relop  5827  acsfn0  17834  cmpsub  23718  ballotlemodife  35130  mh-infprim1bi  37334  mh-infprim2bi  37335  bj-equsvt  37673  bj-sbievw1  37757  bj-sbievw  37759  bj-ralvw  37791  wl-2mintru2  38415  wl-equsalvw  38471  wl-equsald  38472  wl-equsaldv  38473  lub0N  40247  glb0N  40251