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

Theorem mpgbir 1412
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 1408 . 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 1312
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 1408
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  nfi  1421  cvjust  2110  eqriv  2112  abbi2i  2230  nfci  2246  abid2f  2281  rgen  2460  ssriv  3069  ss2abi  3137  nel0  3352  ssmin  3758  intab  3768  iunab  3827  iinab  3842  sndisj  3893  disjxsn  3895  intid  4114  fr0  4241  zfregfr  4456  peano1  4476  relssi  4598  dm0  4721  dmi  4722  funopabeq  5127  isarep2  5178  fvopab3ig  5461  opabex  5610  acexmid  5739  finomni  6978  dfuzi  9112  fzodisj  9895  fzouzdisj  9897  bdelir  12847
  Copyright terms: Public domain W3C validator