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

Theorem mpgbir 1799
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 1795 . 2 𝑥𝜓
3 mpgbir.1 . 2 (𝜑 ↔ ∀𝑥𝜓)
42, 3mpbir 231 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 206  wal 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795
This theorem depends on definitions:  df-bi 207
This theorem is referenced by:  cvjust  2731  eqriv  2734  nfci  2893  abid2f  2936  abid2fOLD  2937  rgen  3063  rabeqcOLD  3690  ssriv  3987  nel0  4354  rab0  4386  ssmin  4967  intab  4978  iunab  5051  iinab  5068  sndisj  5135  disjxsn  5137  abex  5326  intidOLD  5463  fr0  5663  relssi  5797  dmi  5932  dmep  5934  onfr  6423  funopabeq  6602  isarep2  6658  opabiotafun  6989  fvopab3ig  7012  opabex  7240  caovmo  7670  trom  7896  tz7.44lem1  8445  pwfir  9355  dfsup2  9484  zfregfr  9645  dfom3  9687  dfttrcl2  9764  trcl  9768  tc2  9782  rankf  9834  rankval4  9907  uniwun  10780  dfnn2  12279  dfuzi  12709  fzodisj  13733  fzodisjsn  13737  cycsubg  19226  efger  19736  made0  27912  lrrecfr  27976  dfn0s2  28336  ajfuni  30878  funadj  31905  rabexgfGS  32518  abrexdomjm  32526  ballotth  34540  bnj1133  35003  satfv0fun  35376  fmla0xp  35388  dfon3  35893  fnsingle  35920  dfiota3  35924  hftr  36183  bj-rabtrALT  36932  ismblfin  37668  abrexdom  37737  cllem0  43579  cotrintab  43627  brtrclfv2  43740  snhesn  43799  psshepw  43801  k0004val0  44167  scottabf  44259  compab  44461  onfrALT  44569  dvcosre  45927  upwordnul  46895  upwordsing  46899  cfsetssfset  47068  alimp-surprise  49299
  Copyright terms: Public domain W3C validator