Theorem mpgbir 1832

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

This proof depends on syntax axioms:   ↔ wb 209  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210

This theorem is used by:  cvjust  2755  eqriv  2758  nfci  2911  abid2f  2953  abid2fOLD  2954  rgen  3079  ssriv  3935  nel0  4302  rab0OLD  4336  ssmin  4927  intab  4938  sndisj  5095  disjxsn  5097  fr0  5629  relssi  5763  dmi  5903  dmep  5905  onfr  6401  funopabeq  6574  isarep2  6627  opabiotafun  6963  fvopab3ig  6987  opabex  7224  caovmo  7656  funmpt3  7685  trom  7884  tz7.44lem1  8406  pwfir  9301  dfsup2  9429  zfregfr  9598  dfom3  9641  dfttrcl2  9718  trcl  9722  tc2  9734  rankf  9795  rankval4  9877  scottabf  9932  uniwun  10818  dfnn2  12341  dfuzi  12783  fzodisj  13821  fzodisjsn  13825  cycsubg  19416  efger  19925  made0  28242  lrrecfr  28322  dfn0s2  28711  ajfuni  31454  funadj  32481  rabexgfGS  33088  abrexdomjm  33096  ballotth  35163  bnj1133  35612  satfv0fun  36115  fmla0xp  36127  dfon3  36634  fnsingle  36661  dfiota3  36665  hftr  36913  tz9.1tco  37251  dfttc3gw  37291  bj-rabtrALT  37824  ismblfin  38559  abrexdom  38644  cllem0  44551  cotrintab  44599  brtrclfv2  44712  snhesn  44771  psshepw  44773  k0004val0  45139  compab  45410  onfrALT  45517  dvcosre  46891  sinnpoly  47910  cfsetssfset  48095  alimp-surprise  50845