Theorem mpgbir 1801

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

Syntax hints:   ↔ wb 206  ∀wal 1540

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  cvjust  2731  eqriv  2734  nfci  2887  abid2f  2930  abid2fOLD  2931  rgen  3054  ssriv  3926  nel0  4295  rab0  4327  ssmin  4910  intab  4921  sndisj  5078  disjxsn  5080  fr0  5603  relssi  5737  dmi  5871  dmep  5873  onfr  6357  funopabeq  6529  isarep2  6583  opabiotafun  6915  fvopab3ig  6938  opabex  7169  caovmo  7598  trom  7820  tz7.44lem1  8338  pwfir  9221  dfsup2  9351  zfregfr  9519  dfom3  9562  dfttrcl2  9639  trcl  9643  tc2  9655  rankf  9712  rankval4  9785  uniwun  10657  dfnn2  12181  dfuzi  12614  fzodisj  13642  fzodisjsn  13646  cycsubg  19177  efger  19687  made0  27872  lrrecfr  27952  dfn0s2  28341  ajfuni  30948  funadj  31975  rabexgfGS  32587  abrexdomjm  32595  ballotth  34701  bnj1133  35150  satfv0fun  35572  fmla0xp  35584  dfon3  36091  fnsingle  36118  dfiota3  36122  hftr  36383  tz9.1tco  36684  dfttc3gw  36724  bj-rabtrALT  37257  ismblfin  37999  abrexdom  38068  cllem0  44014  cotrintab  44062  brtrclfv2  44175  snhesn  44234  psshepw  44236  k0004val0  44602  scottabf  44688  compab  44889  onfrALT  44997  dvcosre  46361  cfsetssfset  47519  alimp-surprise  50270