Theorem mpgbir 990

Description: Modus ponens on biconditional combined with generalization.

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.1	. . 3 |- (ph <-> A.xps)
2	1	biimpr 152	. 2 |- (A.xps -> ph)
3		mpgbir.2	. 2 |- ps
4	2, 3	mpg 988	1 |- ph

Syntax hints:   <-> wb 146  A.wal 956

This theorem is referenced by:  cvjust 1474  eqriv 1477  abbi2i 1577  abbii 1578  rgen 1701  cbvab 1911  ssriv 2072  ss2abi 2123  ssmin 2556  intab 2564  ssopab2i 2829  fr0 2933  onfr 2992  ordom 3147  relssi 3254  eqrelriv 3257  funopabeq 3555  isarep2 3584  opabex 3615  opabex2g 3617  fvopab3ig 3784  tz7.44lem1 3933  caoprmo 4076  ster 4274  supmo 4585  zfregfr 4610  dfom3 4639  trcl 4655  rankval4 4712  scott0 4727  ac5 4762  1nn 5936  bopcn 7982  sqcn 8331  ajfuni 8516  funadj 9808  abfi 10443  inpc 10476  hst1 10588

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain