New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  mpgbir GIF 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 (φxψ)
mpgbir.2 ψ
Assertion
Ref Expression
mpgbir φ

Proof of Theorem mpgbir
StepHypRef Expression
1 mpgbir.2 . . 3 ψ
21ax-gen 1546 . 2 xψ
3 mpgbir.1 . 2 (φxψ)
42, 3mpbir 200 1 φ
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176  ∀wal 1540 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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