Theorem mpgbir 1800

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

Syntax hints:   ↔ wb 206  ∀wal 1539

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  sbt  2069  cvjust  2725  eqriv  2728  nfci  2882  abid2f  2925  abid2fOLD  2926  rgen  3049  ssriv  3933  nel0  4301  rab0  4333  ssmin  4915  intab  4926  iunab  4998  iinab  5014  sndisj  5081  disjxsn  5083  abex  5262  fr0  5592  relssi  5726  dmi  5860  dmep  5862  onfr  6345  funopabeq  6517  isarep2  6571  opabiotafun  6902  fvopab3ig  6925  opabex  7154  caovmo  7583  trom  7805  tz7.44lem1  8324  pwfir  9201  dfsup2  9328  zfregfr  9494  dfom3  9537  dfttrcl2  9614  trcl  9618  tc2  9630  rankf  9687  rankval4  9760  uniwun  10631  dfnn2  12138  dfuzi  12564  fzodisj  13593  fzodisjsn  13597  cycsubg  19120  efger  19630  made0  27818  lrrecfr  27886  dfn0s2  28260  ajfuni  30839  funadj  31866  rabexgfGS  32479  abrexdomjm  32487  ballotth  34551  bnj1133  35001  satfv0fun  35415  fmla0xp  35427  dfon3  35934  fnsingle  35961  dfiota3  35965  hftr  36224  bj-rabtrALT  36973  ismblfin  37709  abrexdom  37778  cllem0  43607  cotrintab  43655  brtrclfv2  43768  snhesn  43827  psshepw  43829  k0004val0  44195  scottabf  44281  compab  44482  onfrALT  44590  dvcosre  45958  cfsetssfset  47095  alimp-surprise  49820