Theorem mpgbir 1795

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

Syntax hints:   ↔ wb 206  ∀wal 1534

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  cvjust  2728  eqriv  2731  nfci  2890  abid2f  2933  abid2fOLD  2934  rgen  3060  rabeqcOLD  3692  ssriv  3998  nel0  4359  rab0  4391  ssmin  4971  intab  4982  iunab  5055  iinab  5072  sndisj  5139  disjxsn  5141  abex  5331  intidOLD  5468  fr0  5666  relssi  5799  dmi  5934  dmep  5936  onfr  6424  funopabeq  6603  isarep2  6658  opabiotafun  6988  fvopab3ig  7011  opabex  7239  caovmo  7669  trom  7895  tz7.44lem1  8443  pwfir  9352  dfsup2  9481  zfregfr  9642  dfom3  9684  dfttrcl2  9761  trcl  9765  tc2  9779  rankf  9831  rankval4  9904  uniwun  10777  dfnn2  12276  dfuzi  12706  fzodisj  13729  fzodisjsn  13733  cycsubg  19238  efger  19750  made0  27926  lrrecfr  27990  dfn0s2  28350  ajfuni  30887  funadj  31914  rabexgfGS  32526  abrexdomjm  32534  ballotth  34518  bnj1133  34981  satfv0fun  35355  fmla0xp  35367  dfon3  35873  fnsingle  35900  dfiota3  35904  hftr  36163  bj-rabtrALT  36913  ismblfin  37647  abrexdom  37716  cllem0  43555  cotrintab  43603  brtrclfv2  43716  snhesn  43775  psshepw  43777  k0004val0  44143  scottabf  44235  compab  44437  onfrALT  44546  dvcosre  45867  upwordnul  46833  upwordsing  46837  cfsetssfset  47005  alimp-surprise  49010