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  3184  ss2abi  3252  nel0  3469  ssmin  3890  intab  3900  iunab  3960  iinab  3975  sndisj  4026  disjxsn  4028  intid  4254  fr0  4383  zfregfr  4607  peano1  4627  relssi  4751  dm0  4877  dmi  4878  funopabeq  5291  isarep2  5342  fvopab3ig  5632  opabex  5783  acexmid  5918  finomni  7201  dfuzi  9430  fzodisj  10248  fzouzdisj  10250  bdelir  15409