Theorem mpgbir 1446

Description: Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994.) (Proof shortened by Stefan Allan, 28-Oct-2008.)

Hypotheses

Ref	Expression
mpgbir.1	⊢ (𝜑 ↔ ∀𝑥𝜓)
mpgbir.2	⊢ 𝜓

Assertion

Ref	Expression
mpgbir	⊢ 𝜑

Proof of Theorem mpgbir

Step	Hyp	Ref	Expression
1		mpgbir.2	. . 3 ⊢ 𝜓
2	1	ax-gen 1442	. 2 ⊢ ∀𝑥𝜓
3		mpgbir.1	. 2 ⊢ (𝜑 ↔ ∀𝑥𝜓)
4	2, 3	mpbir 145	1 ⊢ 𝜑

Syntax hints:   ↔ wb 104  ∀wal 1346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1442

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nfi  1455  cvjust  2165  eqriv  2167  abbi2i  2285  nfci  2302  abid2f  2338  rgen  2523  ssriv  3151  ss2abi  3219  nel0  3436  ssmin  3850  intab  3860  iunab  3919  iinab  3934  sndisj  3985  disjxsn  3987  intid  4209  fr0  4336  zfregfr  4558  peano1  4578  relssi  4702  dm0  4825  dmi  4826  funopabeq  5234  isarep2  5285  fvopab3ig  5570  opabex  5720  acexmid  5852  finomni  7116  dfuzi  9322  fzodisj  10134  fzouzdisj  10136  bdelir  13882