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 234	1 ⊢ 𝜑

Syntax hints:   ↔ wb 209  ∀wal 1536

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 210

This theorem is referenced by:  cvjust  2793  eqriv  2795  nfci  2939  abid2f  2984  rgen  3116  rabeqc  3626  ssriv  3919  ss2abiOLD  3995  nel0  4264  rab0  4291  abfOLD  4311  ssmin  4857  intab  4868  iunab  4938  iinab  4953  sndisj  5021  disjxsn  5023  intid  5315  fr0  5498  relssi  5624  dmi  5755  dmep  5757  onfr  6198  funopabeq  6360  isarep2  6413  opabiotafun  6719  fvopab3ig  6741  opabex  6960  caovmo  7365  ordom  7569  tz7.44lem1  8024  dfsup2  8892  zfregfr  9052  dfom3  9094  trcl  9154  tc2  9168  rankf  9207  rankval4  9280  uniwun  10151  dfnn2  11638  dfuzi  12061  fzodisj  13066  fzodisjsn  13070  cycsubg  18343  efger  18836  ajfuni  28642  funadj  29669  rabexgfGS  30269  abrexdomjm  30275  ballotth  31905  bnj1133  32371  satfv0fun  32731  fmla0xp  32743  dfon3  33466  fnsingle  33493  dfiota3  33497  hftr  33756  bj-rabtrALT  34373  bj-df-v  34471  wl-rgen  35007  wl-rgenw  35008  ismblfin  35098  abrexdom  35168  cllem0  40265  cotrintab  40314  brtrclfv2  40428  snhesn  40487  psshepw  40489  k0004val0  40857  scottabf  40948  compab  41146  onfrALT  41255  dvcosre  42554  alimp-surprise  45308