Theorem mpgbir 1433

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

Syntax hints:   ↔ wb 104  ∀wal 1333

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 1429

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nfi  1442  cvjust  2152  eqriv  2154  abbi2i  2272  nfci  2289  abid2f  2325  rgen  2510  ssriv  3132  ss2abi  3200  nel0  3415  ssmin  3826  intab  3836  iunab  3895  iinab  3910  sndisj  3961  disjxsn  3963  intid  4183  fr0  4310  zfregfr  4531  peano1  4551  relssi  4674  dm0  4797  dmi  4798  funopabeq  5203  isarep2  5254  fvopab3ig  5539  opabex  5688  acexmid  5817  finomni  7066  dfuzi  9257  fzodisj  10059  fzouzdisj  10061  bdelir  13382