![]() |
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 1790 | . 2 ⊢ ∀𝑥𝜓 |
3 | mpgbir.1 | . 2 ⊢ (𝜑 ↔ ∀𝑥𝜓) | |
4 | 2, 3 | mpbir 230 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∀wal 1532 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 |
This theorem depends on definitions: df-bi 206 |
This theorem is referenced by: cvjust 2720 eqriv 2723 nfci 2879 abid2f 2926 abid2fOLD 2927 rgen 3053 rabeqcOLD 3678 ssriv 3982 nel0 4347 rab0 4380 ssmin 4967 intab 4978 iunab 5051 iinab 5068 sndisj 5136 disjxsn 5138 abex 5323 intidOLD 5456 fr0 5653 relssi 5785 dmi 5920 dmep 5922 onfr 6407 funopabeq 6587 isarep2 6642 opabiotafun 6975 fvopab3ig 6997 opabex 7229 caovmo 7655 trom 7877 tz7.44lem1 8427 pwfir 9350 dfsup2 9480 zfregfr 9641 dfom3 9683 dfttrcl2 9760 trcl 9764 tc2 9778 rankf 9830 rankval4 9903 uniwun 10774 dfnn2 12271 dfuzi 12699 fzodisj 13714 fzodisjsn 13718 cycsubg 19198 efger 19712 made0 27894 lrrecfr 27954 dfn0s2 28301 ajfuni 30789 funadj 31816 rabexgfGS 32424 abrexdomjm 32433 ballotth 34384 bnj1133 34847 satfv0fun 35212 fmla0xp 35224 dfon3 35729 fnsingle 35756 dfiota3 35760 hftr 36019 bj-rabtrALT 36650 ismblfin 37375 abrexdom 37444 cllem0 43270 cotrintab 43318 brtrclfv2 43431 snhesn 43490 psshepw 43492 k0004val0 43858 scottabf 43951 compab 44153 onfrALT 44262 dvcosre 45569 upwordnul 46535 upwordsing 46539 cfsetssfset 46707 alimp-surprise 48564 |
Copyright terms: Public domain | W3C validator |