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  3229  ss2abi  3297  nel0  3514  ssmin  3945  intab  3955  iunab  4015  iinab  4030  sndisj  4082  disjxsn  4084  intid  4314  fr0  4446  zfregfr  4670  peano1  4690  relssi  4815  dm0  4943  dmi  4944  funopabeq  5360  isarep2  5414  fvopab3ig  5716  opabex  5873  acexmid  6012  finomni  7330  dfuzi  9580  fzodisj  10405  fzouzdisj  10407  fzodisjsn  10409  bdelir  16378