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 207

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 208

This theorem is referenced by:  mt2bi  364  pm4.83  1032  trut  1553  equsv  2010  equsalv  2279  equsal  2425  2sb6rf  2481  sb4b  2483  sbequ8  2509  ralv  3457  ceqsal  3468  ceqsalv  3470  sbceqal  3784  relop  5792  acsfn0  17617  cmpsub  23383  ballotlemodife  34682  mh-infprim1bi  36774  mh-infprim2bi  36775  bj-equsvt  37114  bj-sbievw1  37198  bj-sbievw  37200  bj-ralvw  37232  wl-2mintru2  37853  wl-equsalvw  37909  wl-equsald  37910  wl-equsaldv  37911  lub0N  39681  glb0N  39685