Theorem mpgbir 1843

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

Syntax hints:   ↔ wb 198  ∀wal 1599

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

This theorem depends on definitions:  df-bi 199

This theorem is referenced by:  cvjust  2772  cvjustOLD  2773  eqriv  2775  abbi2iOLD  2901  nfci  2922  abid2f  2965  rgen  3104  rabeqc  3570  ssriv  3825  ss2abi  3895  nel0  4160  rab0  4186  abf  4204  ssmin  4729  intab  4740  iunab  4799  iinab  4814  sndisj  4878  disjxsn  4880  intid  5158  fr0  5334  relssi  5458  dmi  5585  onfr  6015  funopabeq  6171  isarep2  6223  opabiotafun  6519  fvopab3ig  6538  opabex  6755  caovmo  7148  ordom  7352  tz7.44lem1  7784  dfsup2  8638  zfregfr  8798  dfom3  8841  trcl  8901  tc2  8915  rankf  8954  rankval4  9027  uniwun  9897  dfnn2  11389  dfuzi  11820  fzodisj  12821  fzodisjsn  12825  cycsubg  18006  efger  18515  ajfuni  28287  funadj  29317  rabexgfGS  29902  abrexdomjm  29907  ballotth  31198  bnj1133  31656  dfon3  32588  fnsingle  32615  dfiota3  32619  hftr  32878  bj-abbi2i  33353  bj-rabtrALT  33501  bj-df-v  33588  ismblfin  34076  abrexdom  34150  cllem0  38828  cotrintab  38878  brtrclfv2  38976  snhesn  39036  psshepw  39038  k0004val0  39408  compab  39600  onfrALT  39709  dvcosre  41054  alimp-surprise  43632