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

Theorem mpgbir 1717
 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 1713 . 2 𝑥𝜓
3 mpgbir.1 . 2 (𝜑 ↔ ∀𝑥𝜓)
42, 3mpbir 220 1 𝜑
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195  ∀wal 1473 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713 This theorem depends on definitions:  df-bi 196 This theorem is referenced by:  nfiOLD  1725  cvjust  2605  eqriv  2607  abbi2i  2725  nfci  2741  abid2f  2777  rgen  2906  ssriv  3572  ss2abi  3637  rab0  3909  abf  3930  ssmin  4431  intab  4442  iunab  4502  iinab  4517  sndisj  4574  disjxsn  4576  intid  4853  fr0  5017  relssi  5134  dm0  5260  dmi  5261  cnv0  5454  onfr  5680  funopabeq  5838  isarep2  5892  opabiotafun  6169  fvopab3ig  6188  opabex  6388  caovmo  6769  ordom  6966  tz7.44lem1  7388  dfsup2  8233  zfregfr  8392  dfom3  8427  trcl  8487  tc2  8501  rankf  8540  rankval4  8613  uniwun  9441  dfnn2  10910  dfuzi  11344  fzodisj  12371  fzouzdisj  12373  fzodisjsn  12374  cycsubg  17445  efger  17954  ajfuni  27099  funadj  28129  rabexgfGS  28725  abrexdomjm  28729  ballotth  29926  bnj1133  30311  dfon3  31169  fnsingle  31196  dfiota3  31200  hftr  31459  bj-abbi2i  31964  bj-rabtrALT  32119  bj-nel0  32128  bj-df-v  32207  ismblfin  32620  abrexdom  32695  cllem0  36890  cotrintab  36940  brtrclfv2  37038  snhesn  37100  psshepw  37102  k0004val0  37472  compab  37666  onfrALT  37785  dvcosre  38799  stoweidlem44  38937  alimp-surprise  42335
 Copyright terms: Public domain W3C validator