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

Theorem mpgbir 1433
 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 1429 . 2 𝑥𝜓
3 mpgbir.1 . 2 (𝜑 ↔ ∀𝑥𝜓)
42, 3mpbir 145 1 𝜑
 Colors of variables: wff set class Syntax hints:   ↔ wb 104  ∀wal 1333 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 1429 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  nfi  1442  cvjust  2152  eqriv  2154  abbi2i  2272  nfci  2289  abid2f  2325  rgen  2510  ssriv  3132  ss2abi  3200  nel0  3415  ssmin  3826  intab  3836  iunab  3895  iinab  3910  sndisj  3961  disjxsn  3963  intid  4183  fr0  4310  zfregfr  4531  peano1  4551  relssi  4674  dm0  4797  dmi  4798  funopabeq  5203  isarep2  5254  fvopab3ig  5539  opabex  5688  acexmid  5817  finomni  7066  dfuzi  9257  fzodisj  10059  fzouzdisj  10061  bdelir  13382
 Copyright terms: Public domain W3C validator