Theorem mpgbir 1831

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

This proof depends on syntax axioms:   ↔ wb 209  ∀wal 1567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827

This proof depends on definitions:  df-bi 210

This theorem is used by:  cvjust  2754  eqriv  2757  nfci  2910  abid2f  2952  abid2fOLD  2953  rgen  3078  ssriv  3913  nel0  4301  rab0OLD  4335  ssmin  4926  intab  4937  sndisj  5094  disjxsn  5096  fr0  5629  relssi  5764  dmi  5904  dmep  5906  onfr  6405  funopabeq  6581  isarep2  6634  opabiotafun  6970  fvopab3ig  6994  opabex  7230  caovmo  7662  funmpt3  7691  trom  7890  tz7.44lem1  8420  pwfir  9315  dfsup2  9443  zfregfr  9612  dfom3  9655  dfttrcl2  9732  trcl  9736  tc2  9748  rankf  9809  rankval4  9891  scottabf  9946  uniwun  10832  dfnn2  12355  dfuzi  12797  fzodisj  13835  fzodisjsn  13839  cycsubg  19432  efger  19941  made0  28258  lrrecfr  28338  dfn0s2  28727  ajfuni  31470  funadj  32497  rabexgfGS  33146  abrexdomjm  33154  ballotth  35220  bnj1133  35669  vsmrep  36013  satfv0fun  36226  fmla0xp  36238  dfon3  36750  fnsingle  36777  dfiota3  36781  hftr  37029  tz9.1tco  37367  dfttc3gw  37407  bj-rabtrALT  37940  ismblfin  38688  abrexdom  38773  cllem0  44676  cotrintab  44723  brtrclfv2  44836  snhesn  44895  psshepw  44897  k0004val0  45263  compab  45533  onfrALT  45640  dvcosre  47030  sinnpoly  48049  cfsetssfset  48234  alimp-surprise  51059