Theorem mpgbir 1794

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

Syntax hints:   ↔ wb 205  ∀wal 1532

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  cvjust  2720  eqriv  2723  nfci  2879  abid2f  2926  abid2fOLD  2927  rgen  3053  rabeqcOLD  3678  ssriv  3982  nel0  4347  rab0  4380  ssmin  4967  intab  4978  iunab  5051  iinab  5068  sndisj  5136  disjxsn  5138  abex  5323  intidOLD  5456  fr0  5653  relssi  5785  dmi  5920  dmep  5922  onfr  6407  funopabeq  6587  isarep2  6642  opabiotafun  6975  fvopab3ig  6997  opabex  7229  caovmo  7655  trom  7877  tz7.44lem1  8427  pwfir  9350  dfsup2  9480  zfregfr  9641  dfom3  9683  dfttrcl2  9760  trcl  9764  tc2  9778  rankf  9830  rankval4  9903  uniwun  10774  dfnn2  12271  dfuzi  12699  fzodisj  13714  fzodisjsn  13718  cycsubg  19198  efger  19712  made0  27894  lrrecfr  27954  dfn0s2  28301  ajfuni  30789  funadj  31816  rabexgfGS  32424  abrexdomjm  32433  ballotth  34384  bnj1133  34847  satfv0fun  35212  fmla0xp  35224  dfon3  35729  fnsingle  35756  dfiota3  35760  hftr  36019  bj-rabtrALT  36650  ismblfin  37375  abrexdom  37444  cllem0  43270  cotrintab  43318  brtrclfv2  43431  snhesn  43490  psshepw  43492  k0004val0  43858  scottabf  43951  compab  44153  onfrALT  44262  dvcosre  45569  upwordnul  46535  upwordsing  46539  cfsetssfset  46707  alimp-surprise  48564