Theorem mpgbir 1464

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

Syntax hints:   ↔ wb 105  ∀wal 1362

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 1460

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfi  1473  cvjust  2188  eqriv  2190  abbi2i  2308  nfci  2326  abid2f  2362  rgen  2547  ssriv  3183  ss2abi  3251  nel0  3468  ssmin  3889  intab  3899  iunab  3959  iinab  3974  sndisj  4025  disjxsn  4027  intid  4253  fr0  4382  zfregfr  4606  peano1  4626  relssi  4750  dm0  4876  dmi  4877  funopabeq  5290  isarep2  5341  fvopab3ig  5631  opabex  5782  acexmid  5917  finomni  7199  dfuzi  9427  fzodisj  10245  fzouzdisj  10247  bdelir  15339