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  1026  trut  1545  equsv  2001  equsalv  2266  equsal  2420  2sb6rf  2476  sb4b  2478  sbequ8  2504  ralv  3485  ceqsal  3496  ceqsalv  3498  sbceqal  3825  relop  5827  acsfn0  17657  cmpsub  23323  ballotlemodife  34438  bj-equsvt  36718  bj-sbievw1  36784  bj-sbievw  36786  bj-ralvw  36818  wl-2mintru2  37430  wl-equsalvw  37477  wl-equsald  37478  wl-equsaldv  37479  lub0N  39128  glb0N  39132