Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpgbir | 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 1425 | . 2 ⊢ ∀𝑥𝜓 |
3 | mpgbir.1 | . 2 ⊢ (𝜑 ↔ ∀𝑥𝜓) | |
4 | 2, 3 | mpbir 145 | 1 ⊢ 𝜑 |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∀wal 1329 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1425 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: nfi 1438 cvjust 2134 eqriv 2136 abbi2i 2254 nfci 2271 abid2f 2306 rgen 2485 ssriv 3101 ss2abi 3169 nel0 3384 ssmin 3790 intab 3800 iunab 3859 iinab 3874 sndisj 3925 disjxsn 3927 intid 4146 fr0 4273 zfregfr 4488 peano1 4508 relssi 4630 dm0 4753 dmi 4754 funopabeq 5159 isarep2 5210 fvopab3ig 5495 opabex 5644 acexmid 5773 finomni 7012 dfuzi 9161 fzodisj 9955 fzouzdisj 9957 bdelir 13045 |
Copyright terms: Public domain | W3C validator |