Theorem mpgbir 1342

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

Syntax hints:   ↔ wb 98  ∀wal 1241

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  nfi  1351  cvjust  2035  eqriv  2037  abbi2i  2152  nfci  2168  abid2f  2202  rgen  2374  ssriv  2949  ss2abi  3012  ssmin  3634  intab  3644  iunab  3703  iinab  3718  sndisj  3760  disjxsn  3762  intid  3960  fr0  4088  zfregfr  4298  peano1  4317  relssi  4431  dm0  4549  dmi  4550  funopabeq  4936  isarep2  4986  fvopab3ig  5246  opabex  5385  acexmid  5511  dfuzi  8348  fzodisj  9034  fzouzdisj  9036  bdelir  9967