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

Theorem mpgbir 1339
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 (φxψ)
mpgbir.2 ψ
Assertion
Ref Expression
mpgbir φ

Proof of Theorem mpgbir
StepHypRef Expression
1 mpgbir.2 . . 3 ψ
21ax-gen 1335 . 2 xψ
3 mpgbir.1 . 2 (φxψ)
42, 3mpbir 134 1 φ
Colors of variables: wff set class
Syntax hints:  wb 98  wal 1240
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1335
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  nfi  1348  cvjust  2032  eqriv  2034  abbi2i  2149  nfci  2165  abid2f  2199  rgen  2368  ssriv  2943  ss2abi  3006  ssmin  3625  intab  3635  iunab  3694  iinab  3709  sndisj  3751  disjxsn  3753  intid  3951  peano1  4260  relssi  4374  dm0  4492  dmi  4493  funopabeq  4879  isarep2  4929  fvopab3ig  5189  opabex  5328  acexmid  5454  dfuzi  8084  fzodisj  8764  fzouzdisj  8766  bdelir  9236
  Copyright terms: Public domain W3C validator