Theorem mpgbir 1502

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

Syntax hints:   ↔ wb 105  ∀wal 1396

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 1498

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfi  1511  cvjust  2229  eqriv  2231  abbi2i  2349  nfci  2376  abid2f  2412  rgen  2597  ssriv  3246  ss2abi  3314  nel0  3534  ssmin  3973  intab  3983  iunab  4043  iinab  4058  sndisj  4110  disjxsn  4112  intid  4345  fr0  4477  zfregfr  4701  peano1  4721  relssi  4846  dm0  4975  dmi  4976  funopabeq  5393  isarep2  5448  fvopab3ig  5756  opabex  5915  acexmid  6057  finomni  7444  dfuzi  9706  fzodisj  10536  fzouzdisj  10538  fzodisjsn  10540  ballotfilemth  13225  bdelir  16743