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 ⊢ 𝜑

Syntax hints:   ↔ wb 105  ∀wal 1400

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 1502

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfi  1515  cvjust  2233  eqriv  2235  abbi2i  2353  nfci  2382  abid2f  2418  rgen  2603  ssriv  3252  ss2abi  3320  nel0  3543  ssmin  3984  intab  3994  iunab  4054  iinab  4069  sndisj  4121  disjxsn  4123  intid  4359  fr0  4491  zfregfr  4716  peano1  4736  relssi  4861  dm0  4990  dmi  4991  funopabeq  5408  isarep2  5463  fvopab3ig  5773  opabex  5932  acexmid  6074  finomni  7470  dfuzi  9735  fzodisj  10565  fzouzdisj  10567  fzodisjsn  10569  ballotfilemth  13259  bdelir  16787