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

Theorem mpgbir 1724
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 1720 . 2 𝑥𝜓
3 mpgbir.1 . 2 (𝜑 ↔ ∀𝑥𝜓)
42, 3mpbir 221 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 196  wal 1479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720
This theorem depends on definitions:  df-bi 197
This theorem is referenced by:  nfiOLD  1732  cvjust  2615  eqriv  2617  abbi2i  2736  nfci  2752  abid2f  2788  rgen  2919  ssriv  3599  ss2abi  3666  nel0  3924  rab0  3946  abf  3969  ssmin  4487  intab  4498  iunab  4557  iinab  4572  sndisj  4635  disjxsn  4637  intid  4917  fr0  5083  relssi  5201  dmi  5329  onfr  5751  funopabeq  5912  isarep2  5966  opabiotafun  6246  fvopab3ig  6265  opabex  6468  caovmo  6856  ordom  7059  tz7.44lem1  7486  dfsup2  8335  zfregfr  8494  dfom3  8529  trcl  8589  tc2  8603  rankf  8642  rankval4  8715  uniwun  9547  dfnn2  11018  dfuzi  11453  fzodisj  12486  fzodisjsn  12489  cycsubg  17603  efger  18112  ajfuni  27685  funadj  28715  rabexgfGS  29312  abrexdomjm  29317  ballotth  30573  bnj1133  31031  dfon3  31974  fnsingle  32001  dfiota3  32005  hftr  32264  bj-abbi2i  32751  bj-rabtrALT  32902  bj-df-v  32991  ismblfin  33421  abrexdom  33496  cllem0  37690  cotrintab  37740  brtrclfv2  37838  snhesn  37900  psshepw  37902  k0004val0  38272  compab  38465  onfrALT  38584  dvcosre  39889  alimp-surprise  42291
  Copyright terms: Public domain W3C validator