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  4129  intid  4366  fr0  4498  zfregfr  4723  peano1  4743  relssi  4868  dm0  4997  dmi  4998  funopabeq  5416  isarep2  5471  fvopab3ig  5782  opabex  5944  acexmid  6087  finomni  7486  dfuzi  9767  fzodisj  10604  fzouzdisj  10606  fzodisjsn  10608  ballotfilemth  13339  bdelir  17078