Theorem mpgbir 1502

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

Syntax hints:   ↔ wb 105  ∀wal 1396

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 1498

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfi  1511  cvjust  2226  eqriv  2228  abbi2i  2346  nfci  2365  abid2f  2401  rgen  2586  ssriv  3232  ss2abi  3300  nel0  3518  ssmin  3952  intab  3962  iunab  4022  iinab  4037  sndisj  4089  disjxsn  4091  intid  4322  fr0  4454  zfregfr  4678  peano1  4698  relssi  4823  dm0  4951  dmi  4952  funopabeq  5369  isarep2  5424  fvopab3ig  5729  opabex  5888  acexmid  6027  finomni  7382  dfuzi  9634  fzodisj  10460  fzouzdisj  10462  fzodisjsn  10464  bdelir  16546