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 1713 | . 2 ⊢ ∀𝑥𝜓 |
3 | mpgbir.1 | . 2 ⊢ (𝜑 ↔ ∀𝑥𝜓) | |
4 | 2, 3 | mpbir 220 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∀wal 1473 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 |
This theorem depends on definitions: df-bi 196 |
This theorem is referenced by: nfiOLD 1725 cvjust 2605 eqriv 2607 abbi2i 2725 nfci 2741 abid2f 2777 rgen 2906 ssriv 3572 ss2abi 3637 rab0 3909 abf 3930 ssmin 4431 intab 4442 iunab 4502 iinab 4517 sndisj 4574 disjxsn 4576 intid 4853 fr0 5017 relssi 5134 dm0 5260 dmi 5261 cnv0 5454 onfr 5680 funopabeq 5838 isarep2 5892 opabiotafun 6169 fvopab3ig 6188 opabex 6388 caovmo 6769 ordom 6966 tz7.44lem1 7388 dfsup2 8233 zfregfr 8392 dfom3 8427 trcl 8487 tc2 8501 rankf 8540 rankval4 8613 uniwun 9441 dfnn2 10910 dfuzi 11344 fzodisj 12371 fzouzdisj 12373 fzodisjsn 12374 cycsubg 17445 efger 17954 ajfuni 27099 funadj 28129 rabexgfGS 28725 abrexdomjm 28729 ballotth 29926 bnj1133 30311 dfon3 31169 fnsingle 31196 dfiota3 31200 hftr 31459 bj-abbi2i 31964 bj-rabtrALT 32119 bj-nel0 32128 bj-df-v 32207 ismblfin 32620 abrexdom 32695 cllem0 36890 cotrintab 36940 brtrclfv2 37038 snhesn 37100 psshepw 37102 k0004val0 37472 compab 37666 onfrALT 37785 dvcosre 38799 stoweidlem44 38937 alimp-surprise 42335 |
Copyright terms: Public domain | W3C validator |