Theorem mpgbir 1806

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

Syntax hints:   ↔ wb 207  ∀wal 1545

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

This theorem depends on definitions:  df-bi 208

This theorem is referenced by:  cvjust  2733  eqriv  2736  nfci  2889  abid2f  2931  abid2fOLD  2932  rgen  3055  ssriv  3919  nel0  4282  rab0  4314  ssmin  4897  intab  4908  sndisj  5064  disjxsn  5066  fr0  5596  relssi  5730  dmi  5863  dmep  5865  onfr  6349  funopabeq  6521  isarep2  6575  opabiotafun  6907  fvopab3ig  6931  opabex  7164  caovmo  7593  trom  7815  tz7.44lem1  8334  pwfir  9217  dfsup2  9347  zfregfr  9516  dfom3  9559  dfttrcl2  9636  trcl  9640  tc2  9652  rankf  9709  rankval4  9782  uniwun  10654  dfnn2  12178  dfuzi  12611  fzodisj  13639  fzodisjsn  13643  cycsubg  19174  efger  19684  made0  27873  lrrecfr  27953  dfn0s2  28342  ajfuni  30948  funadj  31975  rabexgfGS  32587  abrexdomjm  32595  ballotth  34722  bnj1133  35171  satfv0fun  35599  fmla0xp  35611  dfon3  36118  fnsingle  36145  dfiota3  36149  hftr  36410  tz9.1tco  36711  dfttc3gw  36751  bj-rabtrALT  37284  ismblfin  38028  abrexdom  38097  cllem0  44010  cotrintab  44058  brtrclfv2  44171  snhesn  44230  psshepw  44232  k0004val0  44598  scottabf  44684  compab  44885  onfrALT  44993  dvcosre  46355  cfsetssfset  47519  alimp-surprise  50270