Theorem mpgbir 1819

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

Syntax hints:   ↔ wb 208  ∀wal 1558

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

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  cvjust  2756  eqriv  2759  nfci  2912  abid2f  2954  abid2fOLD  2955  rgen  3078  ssriv  3940  nel0  4307  rab0OLD  4340  ssmin  4925  intab  4936  sndisj  5092  disjxsn  5094  fr0  5625  relssi  5759  dmi  5897  dmep  5899  onfr  6385  funopabeq  6557  isarep2  6611  opabiotafun  6947  fvopab3ig  6971  opabex  7204  caovmo  7633  trom  7855  tz7.44lem1  8376  pwfir  9261  dfsup2  9390  zfregfr  9559  dfom3  9602  dfttrcl2  9679  trcl  9683  tc2  9695  rankf  9752  rankval4  9825  uniwun  10698  dfnn2  12223  dfuzi  12664  fzodisj  13699  fzodisjsn  13703  cycsubg  19249  efger  19758  made0  27953  lrrecfr  28033  dfn0s2  28422  ajfuni  31059  funadj  32086  rabexgfGS  32695  abrexdomjm  32703  ballotth  34832  bnj1133  35281  satfv0fun  35718  fmla0xp  35730  dfon3  36237  fnsingle  36264  dfiota3  36268  hftr  36529  tz9.1tco  36840  dfttc3gw  36880  bj-rabtrALT  37413  ismblfin  38157  abrexdom  38226  cllem0  44139  cotrintab  44187  brtrclfv2  44300  snhesn  44359  psshepw  44361  k0004val0  44727  scottabf  44813  compab  45014  onfrALT  45122  dvcosre  46483  cfsetssfset  47647  alimp-surprise  50398