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

Theorem mpgbir 1867
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 1863 . 2 𝑥𝜓
3 mpgbir.1 . 2 (𝜑 ↔ ∀𝑥𝜓)
42, 3mpbir 221 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 196  wal 1622
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863
This theorem depends on definitions:  df-bi 197
This theorem is referenced by:  nfiOLD  1875  cvjust  2747  eqriv  2749  abbi2i  2868  nfci  2884  abid2f  2921  rgen  3052  rabeqc  3494  ssriv  3740  ss2abi  3807  nel0  4067  rab0  4090  abf  4113  ssmin  4640  intab  4651  iunab  4710  iinab  4725  sndisj  4788  disjxsn  4790  intid  5067  fr0  5237  relssi  5360  dmi  5487  onfr  5916  funopabeq  6077  isarep2  6131  opabiotafun  6413  fvopab3ig  6432  opabex  6639  caovmo  7028  ordom  7231  tz7.44lem1  7662  dfsup2  8507  zfregfr  8666  dfom3  8709  trcl  8769  tc2  8783  rankf  8822  rankval4  8895  uniwun  9746  dfnn2  11217  dfuzi  11652  fzodisj  12688  fzodisjsn  12692  cycsubg  17815  efger  18323  ajfuni  28016  funadj  29046  rabexgfGS  29639  abrexdomjm  29644  ballotth  30900  bnj1133  31356  dfon3  32297  fnsingle  32324  dfiota3  32328  hftr  32587  bj-abbi2i  33074  bj-rabtrALT  33225  bj-df-v  33314  ismblfin  33755  abrexdom  33830  cllem0  38365  cotrintab  38415  brtrclfv2  38513  snhesn  38574  psshepw  38576  k0004val0  38946  compab  39139  onfrALT  39258  dvcosre  40621  alimp-surprise  43031
  Copyright terms: Public domain W3C validator