Theorem mpgbir 686

Description: Modus ponens on biconditional combined with generalization.

Hypotheses

Ref	Expression
mpgbir.1	⊢ (φ ↔ ∀xψ)
mpgbir.2	⊢ ψ

Assertion

Ref	Expression
mpgbir	⊢ φ

Proof of Theorem mpgbir

Step	Hyp	Ref	Expression
1		mpgbir.1	. . 3 ⊢ (φ ↔ ∀xψ)
2	1	biimpr 134	. 2 ⊢ (∀xψ → φ)
3		mpgbir.2	. 2 ⊢ ψ
4	2, 3	mpg 684	1 ⊢ φ

Syntax hints:   ↔ wb 127  ∀wal 672

This theorem is referenced by:  cleqri 1101  biabri 1180  biabi 1181  rgen 1247  cbvab 1423  ssriv 1508  ss2abi 1552  ssopab2i 2120  supmo 2156  fr0 2179  onfr 2237  ordom 2382  relssi 2481  cleqreli 2484  funopabeq 2695  funopabex 2742  fvopab3ig 2869  tfrlem8 2956  tz7.44lem1 2965  funoprab 3037  caoprmo 3084  ster 3207  qsex 3231  zfregfr 3452  dfom3 3477  trcl 3489  ranklon 3540  scott0 3542  ac7 3569  ac5 3573  1nn 4432

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

This theorem depends on definitions:  df-bi 128

metamath.org