![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpgbir | Structured version Visualization version GIF version |
Description: Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994.) (Proof shortened by Stefan Allan, 28-Oct-2008.) |
Ref | Expression |
---|---|
mpgbir.1 | ⊢ (𝜑 ↔ ∀𝑥𝜓) |
mpgbir.2 | ⊢ 𝜓 |
Ref | Expression |
---|---|
mpgbir | ⊢ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpgbir.2 | . . 3 ⊢ 𝜓 | |
2 | 1 | ax-gen 1839 | . 2 ⊢ ∀𝑥𝜓 |
3 | mpgbir.1 | . 2 ⊢ (𝜑 ↔ ∀𝑥𝜓) | |
4 | 2, 3 | mpbir 223 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∀wal 1599 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 |
This theorem depends on definitions: df-bi 199 |
This theorem is referenced by: cvjust 2772 cvjustOLD 2773 eqriv 2775 abbi2iOLD 2901 nfci 2922 abid2f 2965 rgen 3104 rabeqc 3570 ssriv 3825 ss2abi 3895 nel0 4160 rab0 4186 abf 4204 ssmin 4729 intab 4740 iunab 4799 iinab 4814 sndisj 4878 disjxsn 4880 intid 5158 fr0 5334 relssi 5458 dmi 5585 onfr 6015 funopabeq 6171 isarep2 6223 opabiotafun 6519 fvopab3ig 6538 opabex 6755 caovmo 7148 ordom 7352 tz7.44lem1 7784 dfsup2 8638 zfregfr 8798 dfom3 8841 trcl 8901 tc2 8915 rankf 8954 rankval4 9027 uniwun 9897 dfnn2 11389 dfuzi 11820 fzodisj 12821 fzodisjsn 12825 cycsubg 18006 efger 18515 ajfuni 28287 funadj 29317 rabexgfGS 29902 abrexdomjm 29907 ballotth 31198 bnj1133 31656 dfon3 32588 fnsingle 32615 dfiota3 32619 hftr 32878 bj-abbi2i 33353 bj-rabtrALT 33501 bj-df-v 33588 ismblfin 34078 abrexdom 34152 cllem0 38832 cotrintab 38882 brtrclfv2 38980 snhesn 39040 psshepw 39042 k0004val0 39412 compab 39604 onfrALT 39713 dvcosre 41058 alimp-surprise 43636 |
Copyright terms: Public domain | W3C validator |