Theorem mpgbir 1475

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

Syntax hints:   ↔ wb 105  ∀wal 1370

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 1471

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfi  1484  cvjust  2199  eqriv  2201  abbi2i  2319  nfci  2337  abid2f  2373  rgen  2558  ssriv  3196  ss2abi  3264  nel0  3481  ssmin  3903  intab  3913  iunab  3973  iinab  3988  sndisj  4039  disjxsn  4041  intid  4267  fr0  4396  zfregfr  4620  peano1  4640  relssi  4764  dm0  4890  dmi  4891  funopabeq  5304  isarep2  5355  fvopab3ig  5647  opabex  5798  acexmid  5933  finomni  7224  dfuzi  9465  fzodisj  10283  fzouzdisj  10285  bdelir  15647