Theorem mpgbir 985

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 983	1 |- ph

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

This theorem is referenced by:  cvjust 1464  eqriv 1467  abbi2i 1566  abbii 1567  rgen 1690  cbvab 1899  ssriv 2059  ss2abi 2110  ssmin 2542  intab 2550  ssopab2i 2812  fr0 2917  onfr 2976  ordom 3131  relssi 3238  eqrelriv 3241  funopabeq 3535  isarep2 3564  opabex 3595  opabex2g 3597  fvopab3ig 3763  tz7.44lem1 3912  caoprmo 4056  ster 4252  supmo 4550  zfregfr 4573  dfom3 4602  trcl 4617  rankval4 4674  scott0 4689  ac5 4724  1nn 5882  bopcn 7919  sqcn 8270  ajfuni 8451  funadj 9730  abfi 10349  hst1 10461

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain