ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpgbir Structured version   Unicode 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
mpgbir.2
Assertion
Ref Expression
mpgbir

Proof of Theorem mpgbir
StepHypRef Expression
1 mpgbir.2 . . 3
21ax-gen 1335 . 2
3 mpgbir.1 . 2
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  8104  fzodisj  8784  fzouzdisj  8786  bdelir  9282
  Copyright terms: Public domain W3C validator