Theorem mpgbir 1501

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

Syntax hints:   ↔ wb 105  ∀wal 1395

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 1497

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfi  1510  cvjust  2226  eqriv  2228  abbi2i  2346  nfci  2364  abid2f  2400  rgen  2585  ssriv  3231  ss2abi  3299  nel0  3516  ssmin  3947  intab  3957  iunab  4017  iinab  4032  sndisj  4084  disjxsn  4086  intid  4316  fr0  4448  zfregfr  4672  peano1  4692  relssi  4817  dm0  4945  dmi  4946  funopabeq  5362  isarep2  5417  fvopab3ig  5720  opabex  5877  acexmid  6016  finomni  7338  dfuzi  9589  fzodisj  10414  fzouzdisj  10416  fzodisjsn  10418  bdelir  16442