NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  mpgbir Unicode version

Theorem mpgbir 1550
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 1546 . 2
3 mpgbir.1 . 2
42, 3mpbir 200 1
Colors of variables: wff setvar class
Syntax hints:   wb 176  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546
This theorem depends on definitions:  df-bi 177
This theorem is referenced by:  nfi  1551  cvjust  2348  eqriv  2350  abbi2i  2464  nfci  2479  abid2f  2514  rgen  2679  ssriv  3277  ss2abi  3338  ssmin  3945  intab  3956  iunab  4012  iinab  4027  nincompl  4072  peano1  4402  addcnul1  4452  ncvspfin  4538  xpvv  4843  relssi  4848  eqrelriv  4850  eqoprriv  4853  dm0  4918  dmi  4919  co01  5093  ssdmrn  5099  funopabeq  5140  funsn  5147  fvopab3ig  5387  1stfo  5505  2ndfo  5506  swapf1o  5511  dmep  5524  caovmo  5645  fnfullfunlem2  5857  fvfullfunlem3  5863  clos1is  5881
  Copyright terms: Public domain W3C validator