ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpgbir Unicode version

Theorem mpgbir 1433
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  |-  ( ph  <->  A. x ps )
mpgbir.2  |-  ps
Assertion
Ref Expression
mpgbir  |-  ph

Proof of Theorem mpgbir
StepHypRef Expression
1 mpgbir.2 . . 3  |-  ps
21ax-gen 1429 . 2  |-  A. x ps
3 mpgbir.1 . 2  |-  ( ph  <->  A. x ps )
42, 3mpbir 145 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 104   A.wal 1333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1429
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  nfi  1442  cvjust  2152  eqriv  2154  abbi2i  2272  nfci  2289  abid2f  2325  rgen  2510  ssriv  3132  ss2abi  3200  nel0  3415  ssmin  3826  intab  3836  iunab  3895  iinab  3910  sndisj  3961  disjxsn  3963  intid  4184  fr0  4311  zfregfr  4533  peano1  4553  relssi  4677  dm0  4800  dmi  4801  funopabeq  5206  isarep2  5257  fvopab3ig  5542  opabex  5691  acexmid  5823  finomni  7083  dfuzi  9274  fzodisj  10077  fzouzdisj  10079  bdelir  13422
  Copyright terms: Public domain W3C validator