Theorem mpgbir 1334

Description: Modus ponens on biconditional combined with generalization. (The proof was shortened by Stefan Allan, 28-Oct-2008.)

Hypotheses

Ref	Expression
mpgbir.1	|- (ph <-> A.xps)
mpgbir.2	|- ps

Assertion

Ref	Expression
mpgbir	|- ph

Proof of Theorem mpgbir

Step	Hyp	Ref	Expression
1		mpgbir.2	. . 3 |- ps
2	1	ax-gen 1305	. 2 |- A.xps
3		mpgbir.1	. 2 |- (ph <-> A.xps)
4	2, 3	mpbir 207	1 |- ph

Syntax hints:   <-> wb 163  A.wal 1296

This theorem is referenced by:  cvjust 1879  eqriv 1881  abbi2i 2005  abbii 2006  abid2f 2012  rgen 2159  ssriv 2621  ss2abi 2679  ssmin 3236  intab 3247  intid 3512  ssopab2i 3574  fr0 3636  dfepfr 3640  onfr 3702  ordom 3960  ordomOLD 3961  relssi 4078  eqrelrivOLD 4081  dm0 4170  dmi 4172  funopabeq 4456  isarep2 4499  opabex 4538  opabex2g 4540  fvopab3ig 4741  fvopab6 4757  caoprmo 5003  tz7.44lem1 5135  ster 5325  supmo 5666  hartog 5693  zfregfr 5706  dfom3 5737  trcl 5752  rankval4 5813  scott0 5847  ac5 5914  1nn 7117  bopcn 9263  vacnlem6 9672  sqcn 9674  ajfuni 9861  abfi 10215  fsubbas 10281  funadj 11450  bnj1062 13397  bnj1077 13405  frxp 13951  dfon3 14072  fnbigcup 14075  limitssson 14080  eqriv2 14281  inpc 14619  dominc 14622  rninc 14623  tolat 14631  hst1 14950  cntrsetlem 14999  domleqt 15020  hartogOLD 15384  abrexdom 15739  fz10 15788

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305

This theorem depends on definitions:  df-bi 164

Copyright terms: Public domain