Theorem mpgbir 1800

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

Syntax hints:   ↔ wb 208  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  cvjust  2818  eqriv  2820  abbi2iOLD  2956  nfci  2966  abid2f  3014  rgen  3150  rabeqc  3680  ssriv  3973  ss2abi  4045  nel0  4313  rab0  4339  abf  4358  ssmin  4897  intab  4908  iunab  4977  iinab  4992  sndisj  5059  disjxsn  5061  intid  5352  fr0  5536  relssi  5662  dmi  5793  dmep  5795  onfr  6232  funopabeq  6393  isarep2  6445  opabiotafun  6746  fvopab3ig  6766  opabex  6985  caovmo  7387  ordom  7591  tz7.44lem1  8043  dfsup2  8910  zfregfr  9070  dfom3  9112  trcl  9172  tc2  9186  rankf  9225  rankval4  9298  uniwun  10164  dfnn2  11653  dfuzi  12076  fzodisj  13074  fzodisjsn  13078  cycsubg  18353  efger  18846  ajfuni  28638  funadj  29665  rabexgfGS  30264  abrexdomjm  30269  ballotth  31797  bnj1133  32263  satfv0fun  32620  fmla0xp  32632  dfon3  33355  fnsingle  33382  dfiota3  33386  hftr  33645  bj-rabtrALT  34251  bj-df-v  34349  wl-rgen  34844  wl-rgenw  34845  ismblfin  34935  abrexdom  35007  cllem0  39932  cotrintab  39981  brtrclfv2  40079  snhesn  40139  psshepw  40141  k0004val0  40511  scottabf  40583  compab  40781  onfrALT  40890  dvcosre  42203  alimp-surprise  44888