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

Theorem mpgbir 1574
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 1570 . 2
3 mpgbir.1 . 2
42, 3mpbir 202 1
Colors of variables: wff set class
Syntax hints:  <->wb 178  A.wal 1564
This theorem is referenced by:  nfi  1575  cvjust  2484  eqriv  2486  abbi2i  2600  nfci  2615  abid2f  2650  rgen  2825  ssriv  3397  ss2abi  3461  ssmin  4173  intab  4184  iunab  4242  iinab  4257  sndisj  4310  disjxsn  4312  intid  4573  fr0  4720  onfr  4779  relssi  4953  dm0  5075  dmi  5076  funopabeq  5472  isarep2  5516  opabiotafun  5768  fvopab3ig  5787  opabex  5961  caovmo  6310  ordom  6495  tz7.44lem1  6825  dfsup2  7614  dfsup2OLD  7615  zfregfr  7737  dfom3  7769  trcl  7831  tc2  7848  rankf  7887  rankval4  7960  uniwun  8786  dfnn2  10201  dfuzi  10596  fzodisj  11435  fzouzdisj  11437  cycsubg  15539  efger  15959  ajfuni  23382  funadj  24412  rabexgfGS  25014  abrexdomjm  25016  ballotth  26070  dfon3  27076  fnsingle  27103  dfiota3  27107  hftr  27462  ismblfin  27612  abrexdom  27804  compab  28871  dvcosre  28966  stoweidlem44  29018  alimp-surprise  29984  onfrALT  30103  bnj1133  30828  bj-nel0  30945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator