Theorem mpgbir 1429

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

Syntax hints:   ↔ wb 104  ∀wal 1329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1425

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nfi  1438  cvjust  2132  eqriv  2134  abbi2i  2252  nfci  2269  abid2f  2304  rgen  2483  ssriv  3096  ss2abi  3164  nel0  3379  ssmin  3785  intab  3795  iunab  3854  iinab  3869  sndisj  3920  disjxsn  3922  intid  4141  fr0  4268  zfregfr  4483  peano1  4503  relssi  4625  dm0  4748  dmi  4749  funopabeq  5154  isarep2  5205  fvopab3ig  5488  opabex  5637  acexmid  5766  finomni  7005  dfuzi  9154  fzodisj  9948  fzouzdisj  9950  bdelir  13034