Theorem mpgbir 1832

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

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

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

This proof depends on definitions:  df-bi 210

This theorem is used by:  cvjust  2757  eqriv  2760  nfci  2914  abid2f  2956  abid2fOLD  2957  rgen  3082  ssriv  3917  nel0  4305  rab0OLD  4339  ssmin  4932  intab  4943  sndisj  5100  disjxsn  5102  fr0  5636  relssi  5772  dmi  5915  dmep  5917  onfr  6428  funopabeq  6604  isarep2  6659  opabiotafun  6996  fvopab3ig  7020  opabex  7257  caovmo  7690  funmpt3  7719  trom  7920  tz7.44lem1  8451  pwfir  9346  dfsup2  9473  zfregfr  9642  dfom3  9685  dfttrcl2  9762  trcl  9766  tc2  9778  rankf  9839  rankval4  9921  scottabf  9976  uniwun  10864  dfnn2  12388  dfuzi  12830  fzodisj  13868  fzodisjsn  13872  cycsubg  19473  efger  19983  made0  28306  lrrecfr  28386  dfn0s2  28775  ajfuni  31518  funadj  32545  rabexgfGS  33194  abrexdomjm  33202  ballotth  35281  bnj1133  35730  jf1o  36052  vsmrep  36131  satfv0fun  36344  fmla0xp  36356  dfon3  36869  fnsingle  36896  dfiota3  36900  hftr  37148  tz9.1tco  37486  dfttc3gw  37526  bj-rabtrALT  38059  ismblfin  38847  abrexdom  38932  cllem0  44828  cotrintab  44875  brtrclfv2  44988  snhesn  45047  psshepw  45049  k0004val0  45415  compab  45685  onfrALT  45792  dvcosre  47195  sinnpoly  48214  cfsetssfset  48399  alimp-surprise  51304