Theorem mpgbir 1477

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 1473	. 2 ⊢ ∀𝑥𝜓
3		mpgbir.1	. 2 ⊢ (𝜑 ↔ ∀𝑥𝜓)
4	2, 3	mpbir 146	1 ⊢ 𝜑

Syntax hints:   ↔ wb 105  ∀wal 1371

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfi  1486  cvjust  2201  eqriv  2203  abbi2i  2321  nfci  2339  abid2f  2375  rgen  2560  ssriv  3201  ss2abi  3269  nel0  3486  ssmin  3910  intab  3920  iunab  3980  iinab  3995  sndisj  4047  disjxsn  4049  intid  4276  fr0  4406  zfregfr  4630  peano1  4650  relssi  4774  dm0  4901  dmi  4902  funopabeq  5316  isarep2  5370  fvopab3ig  5666  opabex  5821  acexmid  5956  finomni  7257  dfuzi  9503  fzodisj  10322  fzouzdisj  10324  fzodisjsn  10326  bdelir  15921