Theorem mpgbir 1829

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

Syntax hints:   ↔ wb 209  ∀wal 1568

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

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  cvjust  2757  eqriv  2760  nfci  2913  abid2f  2955  abid2fOLD  2956  rgen  3081  ssriv  3941  nel0  4309  rab0OLD  4343  ssmin  4932  intab  4943  sndisj  5101  disjxsn  5103  fr0  5639  relssi  5773  dmi  5911  dmep  5913  onfr  6400  funopabeq  6572  isarep2  6625  opabiotafun  6961  fvopab3ig  6985  opabex  7218  caovmo  7647  trom  7867  tz7.44lem1  8388  pwfir  9272  dfsup2  9400  zfregfr  9569  dfom3  9612  dfttrcl2  9689  trcl  9693  tc2  9705  rankf  9762  rankval4  9835  scottabf  9862  uniwun  10720  dfnn2  12241  dfuzi  12682  fzodisj  13718  fzodisjsn  13722  cycsubg  19274  efger  19783  made0  28056  lrrecfr  28136  dfn0s2  28525  ajfuni  31211  funadj  32238  rabexgfGS  32845  abrexdomjm  32853  ballotth  34928  bnj1133  35377  satfv0fun  35863  fmla0xp  35875  dfon3  36382  fnsingle  36409  dfiota3  36413  hftr  36674  tz9.1tco  36994  dfttc3gw  37034  bj-rabtrALT  37567  ismblfin  38312  abrexdom  38381  cllem0  44292  cotrintab  44340  brtrclfv2  44453  snhesn  44512  psshepw  44514  k0004val0  44880  compab  45151  onfrALT  45258  dvcosre  46626  cfsetssfset  47793  alimp-surprise  50558