Theorem mpgbir 1826

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

Syntax hints:   ↔ wb 209  ∀wal 1565

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

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  cvjust  2763  eqriv  2766  nfci  2919  abid2f  2961  abid2fOLD  2962  rgen  3087  ssriv  3949  nel0  4317  rab0OLD  4350  ssmin  4936  intab  4947  sndisj  5105  disjxsn  5107  fr0  5640  relssi  5774  dmi  5912  dmep  5914  onfr  6401  funopabeq  6573  isarep2  6626  opabiotafun  6962  fvopab3ig  6986  opabex  7219  caovmo  7648  trom  7870  tz7.44lem1  8391  pwfir  9275  dfsup2  9403  zfregfr  9572  dfom3  9615  dfttrcl2  9692  trcl  9696  tc2  9708  rankf  9765  rankval4  9838  scottabf  9865  uniwun  10724  dfnn2  12245  dfuzi  12686  fzodisj  13721  fzodisjsn  13725  cycsubg  19278  efger  19787  made0  28021  lrrecfr  28101  dfn0s2  28490  ajfuni  31151  funadj  32178  rabexgfGS  32785  abrexdomjm  32793  ballotth  34872  bnj1133  35321  satfv0fun  35761  fmla0xp  35773  dfon3  36280  fnsingle  36307  dfiota3  36311  hftr  36572  tz9.1tco  36882  dfttc3gw  36922  bj-rabtrALT  37454  ismblfin  38199  abrexdom  38268  cllem0  44183  cotrintab  44231  brtrclfv2  44344  snhesn  44403  psshepw  44405  k0004val0  44771  compab  45042  onfrALT  45149  dvcosre  46517  cfsetssfset  47681  alimp-surprise  50442