Theorem mpgbir 1803

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

Syntax hints:   ↔ wb 205  ∀wal 1537

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  cvjust  2732  eqriv  2735  nfci  2889  abid2f  2938  rgen  3073  rabeqc  3615  ssriv  3921  ss2abiOLD  3997  nel0  4281  rab0  4313  abfOLD  4334  ssmin  4895  intab  4906  iunab  4977  iinab  4993  sndisj  5061  disjxsn  5063  intid  5367  fr0  5559  relssi  5686  dmi  5819  dmep  5821  onfr  6290  funopabeq  6454  isarep2  6507  opabiotafun  6831  fvopab3ig  6853  opabex  7078  caovmo  7487  trom  7696  tz7.44lem1  8207  pwfir  8921  dfsup2  9133  zfregfr  9293  dfom3  9335  trcl  9417  tc2  9431  rankf  9483  rankval4  9556  uniwun  10427  dfnn2  11916  dfuzi  12341  fzodisj  13349  fzodisjsn  13353  cycsubg  18742  efger  19239  ajfuni  29122  funadj  30149  rabexgfGS  30747  abrexdomjm  30753  ballotth  32404  bnj1133  32869  satfv0fun  33233  fmla0xp  33245  dfttrcl2  33710  made0  33984  lrrecfr  34027  dfon3  34121  fnsingle  34148  dfiota3  34152  hftr  34411  bj-rabtrALT  35046  ismblfin  35745  abrexdom  35815  cllem0  41062  cotrintab  41111  brtrclfv2  41224  snhesn  41283  psshepw  41285  k0004val0  41653  scottabf  41747  compab  41949  onfrALT  42058  dvcosre  43343  cfsetssfset  44437  alimp-surprise  46370