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

Theorem mpgbir 1560
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 1556 . 2
3 mpgbir.1 . 2
42, 3mpbir 202 1
Colors of variables: wff set class
Syntax hints:  <->wb 178  A.wal 1550
This theorem is referenced by:  nfi  1561  cvjust  2438  eqriv  2440  abbi2i  2554  nfci  2569  abid2f  2604  rgen  2778  ssriv  3341  ss2abi  3404  ssmin  4098  intab  4109  iunab  4167  iinab  4182  sndisj  4235  disjxsn  4237  intid  4460  fr0  4602  onfr  4661  ordom  4895  relssi  5009  dm0  5127  dmi  5128  funopabeq  5534  isarep2  5580  fvopab3ig  5851  opabex  6012  caovmo  6334  opabiotafun  6586  tz7.44lem1  6712  dfsup2  7496  dfsup2OLD  7497  zfregfr  7619  dfom3  7651  trcl  7713  tc2  7730  rankf  7769  rankval4  7842  uniwun  8666  dfnn2  10064  dfuzi  10411  fzodisj  11218  fzouzdisj  11220  cycsubg  15019  efger  15401  ajfuni  22412  funadj  23440  rabexgfGS  24036  abrexdomjm  24037  ballotth  24899  dfon3  25841  fnsingle  25868  dfiota3  25872  hftr  26227  ismblfin  26356  abrexdom  26543  compab  27799  dvcosre  27895  stoweidlem44  27947  onfrALT  28874  bnj1133  29599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator