Theorem mpgbir 1499

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

Syntax hints:   ↔ wb 105  ∀wal 1393

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 1495

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfi  1508  cvjust  2224  eqriv  2226  abbi2i  2344  nfci  2362  abid2f  2398  rgen  2583  ssriv  3228  ss2abi  3296  nel0  3513  ssmin  3941  intab  3951  iunab  4011  iinab  4026  sndisj  4078  disjxsn  4080  intid  4309  fr0  4441  zfregfr  4665  peano1  4685  relssi  4809  dm0  4936  dmi  4937  funopabeq  5353  isarep2  5407  fvopab3ig  5707  opabex  5862  acexmid  5999  finomni  7303  dfuzi  9553  fzodisj  10372  fzouzdisj  10374  fzodisjsn  10376  bdelir  16168