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

Theorem mpgbir 1446
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 1442 . 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 1346
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 1442
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  nfi  1455  cvjust  2165  eqriv  2167  abbi2i  2285  nfci  2302  abid2f  2338  rgen  2523  ssriv  3151  ss2abi  3219  nel0  3436  ssmin  3850  intab  3860  iunab  3919  iinab  3934  sndisj  3985  disjxsn  3987  intid  4209  fr0  4336  zfregfr  4558  peano1  4578  relssi  4702  dm0  4825  dmi  4826  funopabeq  5234  isarep2  5285  fvopab3ig  5570  opabex  5720  acexmid  5852  finomni  7116  dfuzi  9322  fzodisj  10134  fzouzdisj  10136  bdelir  13882
  Copyright terms: Public domain W3C validator