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  3942  intab  3952  iunab  4012  iinab  4027  sndisj  4079  disjxsn  4081  intid  4310  fr0  4442  zfregfr  4666  peano1  4686  relssi  4810  dm0  4937  dmi  4938  funopabeq  5354  isarep2  5408  fvopab3ig  5710  opabex  5867  acexmid  6006  finomni  7318  dfuzi  9568  fzodisj  10388  fzouzdisj  10390  fzodisjsn  10392  bdelir  16265