Theorem mpgbir 1867

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

Syntax hints:   ↔ wb 196  ∀wal 1622

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

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  nfiOLD  1875  cvjust  2747  eqriv  2749  abbi2i  2868  nfci  2884  abid2f  2921  rgen  3052  rabeqc  3494  ssriv  3740  ss2abi  3807  nel0  4067  rab0  4090  abf  4113  ssmin  4640  intab  4651  iunab  4710  iinab  4725  sndisj  4788  disjxsn  4790  intid  5067  fr0  5237  relssi  5360  dmi  5487  onfr  5916  funopabeq  6077  isarep2  6131  opabiotafun  6413  fvopab3ig  6432  opabex  6639  caovmo  7028  ordom  7231  tz7.44lem1  7662  dfsup2  8507  zfregfr  8666  dfom3  8709  trcl  8769  tc2  8783  rankf  8822  rankval4  8895  uniwun  9746  dfnn2  11217  dfuzi  11652  fzodisj  12688  fzodisjsn  12692  cycsubg  17815  efger  18323  ajfuni  28016  funadj  29046  rabexgfGS  29639  abrexdomjm  29644  ballotth  30900  bnj1133  31356  dfon3  32297  fnsingle  32324  dfiota3  32328  hftr  32587  bj-abbi2i  33074  bj-rabtrALT  33225  bj-df-v  33314  ismblfin  33755  abrexdom  33830  cllem0  38365  cotrintab  38415  brtrclfv2  38513  snhesn  38574  psshepw  38576  k0004val0  38946  compab  39139  onfrALT  39258  dvcosre  40621  alimp-surprise  43031