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  2759  eqriv  2762  nfci  2915  abid2f  2957  abid2fOLD  2958  rgen  3083  ssriv  3942  nel0  4309  rab0OLD  4343  ssmin  4934  intab  4945  sndisj  5103  disjxsn  5105  fr0  5641  relssi  5775  dmi  5913  dmep  5915  onfr  6404  funopabeq  6576  isarep2  6629  opabiotafun  6965  fvopab3ig  6989  opabex  7225  caovmo  7657  trom  7877  tz7.44lem1  8398  pwfir  9283  dfsup2  9411  zfregfr  9580  dfom3  9623  dfttrcl2  9700  trcl  9704  tc2  9716  rankf  9773  rankval4  9846  scottabf  9875  uniwun  10740  dfnn2  12261  dfuzi  12703  fzodisj  13739  fzodisjsn  13743  cycsubg  19323  efger  19832  made0  28107  lrrecfr  28187  dfn0s2  28576  ajfuni  31282  funadj  32309  rabexgfGS  32916  abrexdomjm  32924  ballotth  34993  bnj1133  35442  satfv0fun  35900  fmla0xp  35912  dfon3  36419  fnsingle  36446  dfiota3  36450  hftr  36711  tz9.1tco  37051  dfttc3gw  37091  bj-rabtrALT  37624  ismblfin  38369  abrexdom  38439  cllem0  44350  cotrintab  44398  brtrclfv2  44511  snhesn  44570  psshepw  44572  k0004val0  44938  compab  45209  onfrALT  45316  dvcosre  46684  cfsetssfset  47851  alimp-surprise  50615