Theorem mpgbir 1506

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

This proof depends on syntax axioms:   ↔ wb 105  ∀wal 1400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502

This proof depends on definitions:  df-bi 117

This theorem is used by:  nfi  1515  cvjust  2233  eqriv  2235  abbi2i  2353  nfci  2382  abid2f  2418  rgen  2603  ssriv  3252  ss2abi  3320  nel0  3543  ssmin  3989  intab  3999  iunab  4059  iinab  4074  sndisj  4126  disjxsn  4128  intid  4364  fr0  4496  zfregfr  4721  peano1  4741  relssi  4866  dm0  4995  dmi  4996  funopabeq  5413  isarep2  5468  fvopab3ig  5779  opabex  5941  acexmid  6084  finomni  7480  dfuzi  9756  fzodisj  10587  fzouzdisj  10589  fzodisjsn  10591  ballotfilemth  13281  bdelir  16873