MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpgbir Structured version   Visualization version   GIF version

Theorem mpgbir 1801
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
StepHypRef Expression
1 mpgbir.2 . . 3 𝜓
21ax-gen 1797 . 2 𝑥𝜓
3 mpgbir.1 . 2 (𝜑 ↔ ∀𝑥𝜓)
42, 3mpbir 234 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 209  wal 1536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797
This theorem depends on definitions:  df-bi 210
This theorem is referenced by:  cvjust  2817  eqriv  2819  nfci  2963  abid2f  3008  rgen  3140  rabeqc  3653  ssriv  3946  ss2abi  4018  nel0  4283  rab0  4309  abf  4328  ssmin  4870  intab  4881  iunab  4950  iinab  4965  sndisj  5033  disjxsn  5035  intid  5327  fr0  5511  relssi  5637  dmi  5768  dmep  5770  onfr  6208  funopabeq  6370  isarep2  6422  opabiotafun  6726  fvopab3ig  6746  opabex  6965  caovmo  7370  ordom  7574  tz7.44lem1  8028  dfsup2  8896  zfregfr  9056  dfom3  9098  trcl  9158  tc2  9172  rankf  9211  rankval4  9284  uniwun  10151  dfnn2  11638  dfuzi  12061  fzodisj  13066  fzodisjsn  13070  cycsubg  18342  efger  18835  ajfuni  28640  funadj  29667  rabexgfGS  30267  abrexdomjm  30273  ballotth  31869  bnj1133  32335  satfv0fun  32692  fmla0xp  32704  dfon3  33427  fnsingle  33454  dfiota3  33458  hftr  33717  bj-rabtrALT  34334  bj-df-v  34432  wl-rgen  34965  wl-rgenw  34966  ismblfin  35056  abrexdom  35126  cllem0  40195  cotrintab  40244  brtrclfv2  40358  snhesn  40418  psshepw  40420  k0004val0  40790  scottabf  40882  compab  41080  onfrALT  41189  dvcosre  42493  alimp-surprise  45247
  Copyright terms: Public domain W3C validator