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

Theorem mpgbir 1622
 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 1618 . 2
3 mpgbir.1 . 2
42, 3mpbir 209 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  A.wal 1393 This theorem is referenced by:  nfi  1623  cvjust  2451  eqriv  2453  abbi2i  2590  nfci  2608  abid2f  2648  abid2fOLD  2649  rgen  2817  ssriv  3507  ss2abi  3571  ssmin  4305  intab  4317  iunab  4376  iinab  4391  sndisj  4444  disjxsn  4446  intid  4710  fr0  4863  onfr  4922  relssi  5099  dm0  5221  dmi  5222  funopabeq  5627  isarep2  5673  opabiotafun  5934  fvopab3ig  5953  opabex  6141  caovmo  6512  ordom  6709  tz7.44lem1  7090  dfsup2  7922  dfsup2OLD  7923  zfregfr  8050  dfom3  8085  trcl  8180  tc2  8194  rankf  8233  rankval4  8306  uniwun  9139  dfnn2  10574  dfuzi  10978  fzodisj  11859  fzouzdisj  11861  cycsubg  16229  efger  16736  ajfuni  25775  funadj  26805  rabexgfGS  27401  abrexdomjm  27405  ballotth  28476  dfon3  29542  fnsingle  29569  dfiota3  29573  hftr  29839  ismblfin  30055  abrexdom  30221  compab  31350  dvcosre  31706  stoweidlem44  31826  alimp-surprise  33195  onfrALT  33321  bnj1133  34045  bj-abbi2i  34362  bj-rabtrALT  34498  bj-nel0  34504  bj-df-v  34583  cllem0  37751  snhesn  37809  psshepw  37811 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618 This theorem depends on definitions:  df-bi 185
 Copyright terms: Public domain W3C validator