MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpgbir Unicode version

Theorem mpgbir 1540
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 1536 . 2  |-  A. x ps
3 mpgbir.1 . 2  |-  ( ph  <->  A. x ps )
42, 3mpbir 200 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1530
This theorem is referenced by:  nfi  1541  cvjust  2291  eqriv  2293  abbi2i  2407  nfci  2422  abid2f  2457  rgen  2621  ssriv  3197  ss2abi  3258  ssmin  3897  intab  3908  iunab  3964  iinab  3979  sndisj  4031  disjxsn  4033  intid  4247  fr0  4388  onfr  4447  ordom  4681  relssi  4794  dm0  4908  dmi  4909  funopabeq  5304  isarep2  5348  fvopab3ig  5615  opabex  5760  caovmo  6073  opabiotafun  6307  tz7.44lem1  6434  dfsup2  7211  dfsup2OLD  7212  zfregfr  7332  dfom3  7364  trcl  7426  tc2  7443  rankf  7482  rankval4  7555  uniwun  8378  dfnn2  9775  dfuzi  10118  fzodisj  10916  fzouzdisj  10918  cycsubg  14661  efger  15043  ajfuni  21454  funadj  22482  abrexdomjm  23181  dfon3  24503  fnsingle  24529  dfiota3  24533  hftr  24884  eqriv2  25050  eqint  25063  inpc  25380  dominc  25383  rninc  25384  pgapspf  26155  abrexdom  26508  compab  27747  onfrALT  28613  bnj1133  29335
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator