Theorem mpgbir 1805

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

Syntax hints:   ↔ wb 205  ∀wal 1539

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  cvjust  2733  eqriv  2736  nfci  2891  abid2f  2940  rgen  3075  rabeqc  3623  ssriv  3929  ss2abiOLD  4005  nel0  4289  rab0  4321  abfOLD  4342  ssmin  4903  intab  4914  iunab  4985  iinab  5001  sndisj  5069  disjxsn  5071  intid  5375  fr0  5567  relssi  5694  dmi  5827  dmep  5829  onfr  6302  funopabeq  6466  isarep2  6519  opabiotafun  6843  fvopab3ig  6865  opabex  7090  caovmo  7500  trom  7709  tz7.44lem1  8220  pwfir  8924  dfsup2  9164  zfregfr  9324  dfom3  9366  dfttrcl2  9443  trcl  9469  tc2  9483  rankf  9536  rankval4  9609  uniwun  10480  dfnn2  11969  dfuzi  12394  fzodisj  13402  fzodisjsn  13406  cycsubg  18808  efger  19305  ajfuni  29200  funadj  30227  rabexgfGS  30825  abrexdomjm  30831  ballotth  32483  bnj1133  32948  satfv0fun  33312  fmla0xp  33324  made0  34036  lrrecfr  34079  dfon3  34173  fnsingle  34200  dfiota3  34204  hftr  34463  bj-rabtrALT  35098  ismblfin  35797  abrexdom  35867  cllem0  41126  cotrintab  41175  brtrclfv2  41288  snhesn  41347  psshepw  41349  k0004val0  41717  scottabf  41811  compab  42013  onfrALT  42122  dvcosre  43407  cfsetssfset  44501  alimp-surprise  46436  upwordnul  46464