Theorem mpgbir 1441

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

Syntax hints:   ↔ wb 104  ∀wal 1341

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 1437

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nfi  1450  cvjust  2160  eqriv  2162  abbi2i  2281  nfci  2298  abid2f  2334  rgen  2519  ssriv  3146  ss2abi  3214  nel0  3430  ssmin  3843  intab  3853  iunab  3912  iinab  3927  sndisj  3978  disjxsn  3980  intid  4202  fr0  4329  zfregfr  4551  peano1  4571  relssi  4695  dm0  4818  dmi  4819  funopabeq  5224  isarep2  5275  fvopab3ig  5560  opabex  5709  acexmid  5841  finomni  7104  dfuzi  9301  fzodisj  10113  fzouzdisj  10115  bdelir  13729