Theorem mpgbir 1799

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

Syntax hints:   ↔ wb 206  ∀wal 1538

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  sbt  2067  cvjust  2723  eqriv  2726  nfci  2879  abid2f  2922  abid2fOLD  2923  rgen  3046  rabeqcOLD  3646  ssriv  3939  nel0  4305  rab0  4337  ssmin  4917  intab  4928  iunab  5000  iinab  5017  sndisj  5084  disjxsn  5086  abex  5265  intidOLD  5401  fr0  5597  relssi  5730  dmi  5864  dmep  5866  onfr  6346  funopabeq  6518  isarep2  6572  opabiotafun  6903  fvopab3ig  6926  opabex  7156  caovmo  7586  trom  7808  tz7.44lem1  8327  pwfir  9206  dfsup2  9334  zfregfr  9500  dfom3  9543  dfttrcl2  9620  trcl  9624  tc2  9638  rankf  9690  rankval4  9763  uniwun  10634  dfnn2  12141  dfuzi  12567  fzodisj  13596  fzodisjsn  13600  cycsubg  19087  efger  19597  made0  27787  lrrecfr  27855  dfn0s2  28229  ajfuni  30803  funadj  31830  rabexgfGS  32443  abrexdomjm  32451  ballotth  34506  bnj1133  34956  satfv0fun  35344  fmla0xp  35356  dfon3  35866  fnsingle  35893  dfiota3  35897  hftr  36156  bj-rabtrALT  36905  ismblfin  37641  abrexdom  37710  cllem0  43539  cotrintab  43587  brtrclfv2  43700  snhesn  43759  psshepw  43761  k0004val0  44127  scottabf  44213  compab  44415  onfrALT  44523  dvcosre  45893  upwordnul  46861  upwordsing  46865  cfsetssfset  47040  alimp-surprise  49765