![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mprgbir | GIF version |
Description: Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.) |
Ref | Expression |
---|---|
mprgbir.1 | ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) |
mprgbir.2 | ⊢ (𝑥 ∈ 𝐴 → 𝜓) |
Ref | Expression |
---|---|
mprgbir | ⊢ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mprgbir.2 | . . 3 ⊢ (𝑥 ∈ 𝐴 → 𝜓) | |
2 | 1 | rgen 2543 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝜓 |
3 | mprgbir.1 | . 2 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) | |
4 | 2, 3 | mpbir 146 | 1 ⊢ 𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 ∈ wcel 2160 ∀wral 2468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-gen 1460 |
This theorem depends on definitions: df-bi 117 df-ral 2473 |
This theorem is referenced by: ss2rabi 3252 rabnc 3470 ssintub 3877 tron 4400 djussxp 4790 dmiin 4891 dfco2 5146 coiun 5156 tfrlem6 6340 oacl 6484 sbthlem1 6985 peano1nnnn 7880 renfdisj 8046 1nn 8959 ioomax 9977 iccmax 9978 fxnn0nninf 10468 fisumcom2 11477 fprodcom2fi 11665 bezoutlemmain 12030 dfphi2 12251 unennn 12447 znnen 12448 istopon 13965 neipsm 14106 bj-omtrans2 15162 nninfomnilem 15221 exmidsbthrlem 15224 |
Copyright terms: Public domain | W3C validator |