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 231	1 ⊢ 𝜑

Syntax hints:   ↔ wb 206  ∀wal 1539

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 207

This theorem is referenced by:  cvjust  2730  eqriv  2733  nfci  2886  abid2f  2929  abid2fOLD  2930  rgen  3053  ssriv  3937  nel0  4306  rab0  4338  ssmin  4922  intab  4933  iunab  5007  iinab  5023  sndisj  5090  disjxsn  5092  fr0  5602  relssi  5736  dmi  5870  dmep  5872  onfr  6356  funopabeq  6528  isarep2  6582  opabiotafun  6914  fvopab3ig  6937  opabex  7166  caovmo  7595  trom  7817  tz7.44lem1  8336  pwfir  9217  dfsup2  9347  zfregfr  9513  dfom3  9556  dfttrcl2  9633  trcl  9637  tc2  9649  rankf  9706  rankval4  9779  uniwun  10651  dfnn2  12158  dfuzi  12583  fzodisj  13609  fzodisjsn  13613  cycsubg  19137  efger  19647  made0  27859  lrrecfr  27939  dfn0s2  28328  ajfuni  30934  funadj  31961  rabexgfGS  32574  abrexdomjm  32582  ballotth  34695  bnj1133  35145  satfv0fun  35565  fmla0xp  35577  dfon3  36084  fnsingle  36111  dfiota3  36115  hftr  36376  bj-rabtrALT  37132  ismblfin  37862  abrexdom  37931  cllem0  43807  cotrintab  43855  brtrclfv2  43968  snhesn  44027  psshepw  44029  k0004val0  44395  scottabf  44481  compab  44682  onfrALT  44790  dvcosre  46156  cfsetssfset  47302  alimp-surprise  50025