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  4397  zfregfr  4621  peano1  4641  relssi  4765  dm0  4891  dmi  4892  funopabeq  5306  isarep2  5360  fvopab3ig  5652  opabex  5807  acexmid  5942  finomni  7241  dfuzi  9482  fzodisj  10300  fzouzdisj  10302  bdelir  15716