| 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 1795 | . 2 ⊢ ∀𝑥𝜓 |
| 3 | mpgbir.1 | . 2 ⊢ (𝜑 ↔ ∀𝑥𝜓) | |
| 4 | 2, 3 | mpbir 231 | 1 ⊢ 𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∀wal 1538 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 |
| This theorem depends on definitions: df-bi 207 |
| This theorem is referenced by: cvjust 2731 eqriv 2734 nfci 2893 abid2f 2936 abid2fOLD 2937 rgen 3063 rabeqcOLD 3690 ssriv 3987 nel0 4354 rab0 4386 ssmin 4967 intab 4978 iunab 5051 iinab 5068 sndisj 5135 disjxsn 5137 abex 5326 intidOLD 5463 fr0 5663 relssi 5797 dmi 5932 dmep 5934 onfr 6423 funopabeq 6602 isarep2 6658 opabiotafun 6989 fvopab3ig 7012 opabex 7240 caovmo 7670 trom 7896 tz7.44lem1 8445 pwfir 9355 dfsup2 9484 zfregfr 9645 dfom3 9687 dfttrcl2 9764 trcl 9768 tc2 9782 rankf 9834 rankval4 9907 uniwun 10780 dfnn2 12279 dfuzi 12709 fzodisj 13733 fzodisjsn 13737 cycsubg 19226 efger 19736 made0 27912 lrrecfr 27976 dfn0s2 28336 ajfuni 30878 funadj 31905 rabexgfGS 32518 abrexdomjm 32526 ballotth 34540 bnj1133 35003 satfv0fun 35376 fmla0xp 35388 dfon3 35893 fnsingle 35920 dfiota3 35924 hftr 36183 bj-rabtrALT 36932 ismblfin 37668 abrexdom 37737 cllem0 43579 cotrintab 43627 brtrclfv2 43740 snhesn 43799 psshepw 43801 k0004val0 44167 scottabf 44259 compab 44461 onfrALT 44569 dvcosre 45927 upwordnul 46895 upwordsing 46899 cfsetssfset 47068 alimp-surprise 49299 |
| Copyright terms: Public domain | W3C validator |