Theorem mpgbir 1382

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

Syntax hints:   ↔ wb 103  ∀wal 1282

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  nfi  1391  cvjust  2076  eqriv  2078  abbi2i  2193  nfci  2209  abid2f  2243  rgen  2416  ssriv  3003  ss2abi  3066  ssmin  3655  intab  3665  iunab  3724  iinab  3739  sndisj  3781  disjxsn  3783  intid  3979  fr0  4106  zfregfr  4316  peano1  4335  relssi  4449  dm0  4567  dmi  4568  funopabeq  4956  isarep2  5006  fvopab3ig  5267  opabex  5406  acexmid  5531  dfuzi  8457  fzodisj  9187  fzouzdisj  9189  bdelir  10638