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

Theorem mpgbir 1383
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 1379 . 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 1283
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 1379
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  nfi  1392  cvjust  2077  eqriv  2079  abbi2i  2194  nfci  2210  abid2f  2244  rgen  2417  ssriv  3004  ss2abi  3067  ssmin  3663  intab  3673  iunab  3732  iinab  3747  sndisj  3789  disjxsn  3791  intid  3987  fr0  4114  zfregfr  4324  peano1  4343  relssi  4457  dm0  4577  dmi  4578  funopabeq  4966  isarep2  5017  fvopab3ig  5278  opabex  5417  acexmid  5542  dfuzi  8538  fzodisj  9264  fzouzdisj  9266  bdelir  10796
  Copyright terms: Public domain W3C validator