Theorem mpgbir 1430

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

Syntax hints:   ↔ wb 104  ∀wal 1330

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 1426

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nfi  1439  cvjust  2135  eqriv  2137  abbi2i  2255  nfci  2272  abid2f  2307  rgen  2488  ssriv  3106  ss2abi  3174  nel0  3389  ssmin  3798  intab  3808  iunab  3867  iinab  3882  sndisj  3933  disjxsn  3935  intid  4154  fr0  4281  zfregfr  4496  peano1  4516  relssi  4638  dm0  4761  dmi  4762  funopabeq  5167  isarep2  5218  fvopab3ig  5503  opabex  5652  acexmid  5781  finomni  7020  dfuzi  9185  fzodisj  9986  fzouzdisj  9988  bdelir  13216