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 1338 | . 2 ⊢ ∀𝑥𝜓 |
3 | mpgbir.1 | . 2 ⊢ (𝜑 ↔ ∀𝑥𝜓) | |
4 | 2, 3 | mpbir 134 | 1 ⊢ 𝜑 |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 ∀wal 1241 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-gen 1338 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: nfi 1351 cvjust 2035 eqriv 2037 abbi2i 2152 nfci 2168 abid2f 2202 rgen 2374 ssriv 2949 ss2abi 3012 ssmin 3634 intab 3644 iunab 3703 iinab 3718 sndisj 3760 disjxsn 3762 intid 3960 fr0 4088 zfregfr 4298 peano1 4317 relssi 4431 dm0 4549 dmi 4550 funopabeq 4936 isarep2 4986 fvopab3ig 5246 opabex 5385 acexmid 5511 dfuzi 8348 fzodisj 9034 fzouzdisj 9036 bdelir 9967 |
Copyright terms: Public domain | W3C validator |