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

Theorem mpgbir 1566
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 1562 . 2
3 mpgbir.1 . 2
42, 3mpbir 202 1
Colors of variables: wff set class
Syntax hints:  <->wb 178  A.wal 1556
This theorem is referenced by:  nfi  1567  cvjust  2476  eqriv  2478  abbi2i  2592  nfci  2607  abid2f  2642  rgen  2817  ssriv  3385  ss2abi  3448  ssmin  4157  intab  4168  iunab  4226  iinab  4241  sndisj  4294  disjxsn  4296  intid  4557  fr0  4702  onfr  4761  relssi  4935  dm0  5057  dmi  5058  funopabeq  5451  isarep2  5495  opabiotafun  5745  fvopab3ig  5764  opabex  5925  caovmo  6267  ordom  6450  tz7.44lem1  6775  dfsup2  7559  dfsup2OLD  7560  zfregfr  7682  dfom3  7714  trcl  7776  tc2  7793  rankf  7832  rankval4  7905  uniwun  8729  dfnn2  10144  dfuzi  10539  fzodisj  11378  fzouzdisj  11380  cycsubg  15471  efger  15853  ajfuni  22870  funadj  23900  rabexgfGS  24502  abrexdomjm  24504  ballotth  25561  dfon3  26567  fnsingle  26594  dfiota3  26598  hftr  26953  ismblfin  27103  abrexdom  27295  compab  28546  dvcosre  28641  stoweidlem44  28693  alimp-surprise  29707  onfrALT  29826  bnj1133  30551  bj-nel0  30668
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator