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  2754  eqriv  2757  nfci  2910  abid2f  2952  abid2fOLD  2953  rgen  3078  ssriv  3935  nel0  4302  rab0OLD  4336  ssmin  4927  intab  4938  sndisj  5095  disjxsn  5097  fr0  5633  relssi  5767  dmi  5905  dmep  5907  onfr  6397  funopabeq  6569  isarep2  6622  opabiotafun  6958  fvopab3ig  6982  opabex  7219  caovmo  7651  trom  7871  tz7.44lem1  8394  pwfir  9286  dfsup2  9414  zfregfr  9583  dfom3  9626  dfttrcl2  9703  trcl  9707  tc2  9719  rankf  9776  rankval4  9849  scottabf  9878  uniwun  10749  dfnn2  12270  dfuzi  12712  fzodisj  13749  fzodisjsn  13753  cycsubg  19336  efger  19845  made0  28128  lrrecfr  28208  dfn0s2  28597  ajfuni  31340  funadj  32367  rabexgfGS  32974  abrexdomjm  32982  ballotth  35049  bnj1133  35498  satfv0fun  35950  fmla0xp  35962  dfon3  36469  fnsingle  36496  dfiota3  36500  hftr  36762  tz9.1tco  37102  dfttc3gw  37142  bj-rabtrALT  37675  ismblfin  38410  abrexdom  38480  cllem0  44406  cotrintab  44454  brtrclfv2  44567  snhesn  44626  psshepw  44628  k0004val0  44994  compab  45265  onfrALT  45372  dvcosre  46740  sinnpoly  47759  cfsetssfset  47944  alimp-surprise  50709