Theorem mpgbir 1799

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

Syntax hints:   ↔ wb 206  ∀wal 1538

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  cvjust  2731  eqriv  2734  nfci  2893  abid2f  2936  abid2fOLD  2937  rgen  3063  rabeqcOLD  3690  ssriv  3987  nel0  4354  rab0  4386  ssmin  4967  intab  4978  iunab  5051  iinab  5068  sndisj  5135  disjxsn  5137  abex  5326  intidOLD  5463  fr0  5663  relssi  5797  dmi  5932  dmep  5934  onfr  6423  funopabeq  6602  isarep2  6658  opabiotafun  6989  fvopab3ig  7012  opabex  7240  caovmo  7670  trom  7896  tz7.44lem1  8445  pwfir  9355  dfsup2  9484  zfregfr  9645  dfom3  9687  dfttrcl2  9764  trcl  9768  tc2  9782  rankf  9834  rankval4  9907  uniwun  10780  dfnn2  12279  dfuzi  12709  fzodisj  13733  fzodisjsn  13737  cycsubg  19226  efger  19736  made0  27912  lrrecfr  27976  dfn0s2  28336  ajfuni  30878  funadj  31905  rabexgfGS  32518  abrexdomjm  32526  ballotth  34540  bnj1133  35003  satfv0fun  35376  fmla0xp  35388  dfon3  35893  fnsingle  35920  dfiota3  35924  hftr  36183  bj-rabtrALT  36932  ismblfin  37668  abrexdom  37737  cllem0  43579  cotrintab  43627  brtrclfv2  43740  snhesn  43799  psshepw  43801  k0004val0  44167  scottabf  44259  compab  44461  onfrALT  44569  dvcosre  45927  upwordnul  46895  upwordsing  46899  cfsetssfset  47068  alimp-surprise  49299