Theorem mpgbir 1453

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

Syntax hints:   ↔ wb 105  ∀wal 1351

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 1449

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfi  1462  cvjust  2172  eqriv  2174  abbi2i  2292  nfci  2309  abid2f  2345  rgen  2530  ssriv  3160  ss2abi  3228  nel0  3445  ssmin  3864  intab  3874  iunab  3934  iinab  3949  sndisj  4000  disjxsn  4002  intid  4225  fr0  4352  zfregfr  4574  peano1  4594  relssi  4718  dm0  4842  dmi  4843  funopabeq  5253  isarep2  5304  fvopab3ig  5591  opabex  5741  acexmid  5874  finomni  7138  dfuzi  9363  fzodisj  10178  fzouzdisj  10180  bdelir  14602