Theorem mpgbir 1388

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

Syntax hints:   ↔ wb 104  ∀wal 1288

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nfi  1397  cvjust  2084  eqriv  2086  abbi2i  2203  nfci  2219  abid2f  2254  rgen  2429  ssriv  3030  ss2abi  3094  nel0  3308  ssmin  3713  intab  3723  iunab  3782  iinab  3797  sndisj  3847  disjxsn  3849  intid  4060  fr0  4187  zfregfr  4402  peano1  4422  relssi  4542  dm0  4663  dmi  4664  funopabeq  5063  isarep2  5114  fvopab3ig  5391  opabex  5535  acexmid  5665  finomni  6857  dfuzi  8917  fzodisj  9650  fzouzdisj  9652  bdelir  12011