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

Theorem mpgbir 1387
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 1383 . 2  |-  A. x ps
3 mpgbir.1 . 2  |-  ( ph  <->  A. x ps )
42, 3mpbir 144 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 103   A.wal 1287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1383
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  nfi  1396  cvjust  2083  eqriv  2085  abbi2i  2202  nfci  2218  abid2f  2253  rgen  2428  ssriv  3027  ss2abi  3091  nel0  3302  ssmin  3702  intab  3712  iunab  3771  iinab  3786  sndisj  3833  disjxsn  3835  intid  4042  fr0  4169  zfregfr  4379  peano1  4399  relssi  4517  dm0  4638  dmi  4639  funopabeq  5036  isarep2  5087  fvopab3ig  5362  opabex  5503  acexmid  5633  finomni  6775  dfuzi  8826  fzodisj  9554  fzouzdisj  9556  bdelir  11395
  Copyright terms: Public domain W3C validator