Theorem mpgbir 1802

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

Syntax hints:   ↔ wb 205  ∀wal 1540

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  cvjust  2727  eqriv  2730  nfci  2887  abid2f  2937  abid2fOLD  2938  rgen  3064  rabeqcOLD  3682  ssriv  3987  ss2abiOLD  4065  nel0  4351  rab0  4383  abfOLD  4404  ssmin  4972  intab  4983  iunab  5055  iinab  5072  sndisj  5140  disjxsn  5142  intidOLD  5459  fr0  5656  relssi  5788  dmi  5922  dmep  5924  onfr  6404  funopabeq  6585  isarep2  6640  opabiotafun  6973  fvopab3ig  6995  opabex  7222  caovmo  7644  trom  7864  tz7.44lem1  8405  pwfir  9176  dfsup2  9439  zfregfr  9600  dfom3  9642  dfttrcl2  9719  trcl  9723  tc2  9737  rankf  9789  rankval4  9862  uniwun  10735  dfnn2  12225  dfuzi  12653  fzodisj  13666  fzodisjsn  13670  cycsubg  19085  efger  19586  made0  27369  lrrecfr  27429  dfn0s2  27705  ajfuni  30143  funadj  31170  rabexgfGS  31770  abrexdomjm  31775  ballotth  33567  bnj1133  34031  satfv0fun  34393  fmla0xp  34405  dfon3  34895  fnsingle  34922  dfiota3  34926  hftr  35185  bj-rabtrALT  35859  ismblfin  36577  abrexdom  36646  cllem0  42365  cotrintab  42413  brtrclfv2  42526  snhesn  42585  psshepw  42587  k0004val0  42953  scottabf  43047  compab  43249  onfrALT  43358  dvcosre  44676  upwordnul  45642  upwordsing  45646  cfsetssfset  45814  alimp-surprise  47875