Theorem mpgbir 1502

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

Syntax hints:   ↔ wb 105  ∀wal 1396

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 1498

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfi  1511  cvjust  2227  eqriv  2229  abbi2i  2347  nfci  2374  abid2f  2410  rgen  2595  ssriv  3242  ss2abi  3310  nel0  3530  ssmin  3968  intab  3978  iunab  4038  iinab  4053  sndisj  4105  disjxsn  4107  intid  4340  fr0  4472  zfregfr  4696  peano1  4716  relssi  4841  dm0  4970  dmi  4971  funopabeq  5388  isarep2  5443  fvopab3ig  5751  opabex  5910  acexmid  6049  finomni  7431  dfuzi  9688  fzodisj  10514  fzouzdisj  10516  fzodisjsn  10518  bdelir  16617