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  3681  ssriv  3986  ss2abiOLD  4064  nel0  4350  rab0  4382  abfOLD  4403  ssmin  4971  intab  4982  iunab  5054  iinab  5071  sndisj  5139  disjxsn  5141  intidOLD  5458  fr0  5655  relssi  5786  dmi  5920  dmep  5922  onfr  6401  funopabeq  6582  isarep2  6637  opabiotafun  6970  fvopab3ig  6992  opabex  7219  caovmo  7641  trom  7861  tz7.44lem1  8402  pwfir  9173  dfsup2  9436  zfregfr  9597  dfom3  9639  dfttrcl2  9716  trcl  9720  tc2  9734  rankf  9786  rankval4  9859  uniwun  10732  dfnn2  12222  dfuzi  12650  fzodisj  13663  fzodisjsn  13667  cycsubg  19080  efger  19581  made0  27358  lrrecfr  27417  ajfuni  30100  funadj  31127  rabexgfGS  31727  abrexdomjm  31732  ballotth  33525  bnj1133  33989  satfv0fun  34351  fmla0xp  34363  dfon3  34853  fnsingle  34880  dfiota3  34884  hftr  35143  bj-rabtrALT  35800  ismblfin  36518  abrexdom  36587  cllem0  42303  cotrintab  42351  brtrclfv2  42464  snhesn  42523  psshepw  42525  k0004val0  42891  scottabf  42985  compab  43187  onfrALT  43296  dvcosre  44615  upwordnul  45581  upwordsing  45585  cfsetssfset  45753  alimp-surprise  47781