Theorem mpgbir 1467

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 1463	. 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 1463

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfi  1476  cvjust  2191  eqriv  2193  abbi2i  2311  nfci  2329  abid2f  2365  rgen  2550  ssriv  3187  ss2abi  3255  nel0  3472  ssmin  3893  intab  3903  iunab  3963  iinab  3978  sndisj  4029  disjxsn  4031  intid  4257  fr0  4386  zfregfr  4610  peano1  4630  relssi  4754  dm0  4880  dmi  4881  funopabeq  5294  isarep2  5345  fvopab3ig  5635  opabex  5786  acexmid  5921  finomni  7206  dfuzi  9436  fzodisj  10254  fzouzdisj  10256  bdelir  15493