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  3188  ss2abi  3256  nel0  3473  ssmin  3894  intab  3904  iunab  3964  iinab  3979  sndisj  4030  disjxsn  4032  intid  4258  fr0  4387  zfregfr  4611  peano1  4631  relssi  4755  dm0  4881  dmi  4882  funopabeq  5295  isarep2  5346  fvopab3ig  5638  opabex  5789  acexmid  5924  finomni  7215  dfuzi  9453  fzodisj  10271  fzouzdisj  10273  bdelir  15577