![]() |
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 2444 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝜓 |
3 | mprgbir.1 | . 2 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) | |
4 | 2, 3 | mpbir 145 | 1 ⊢ 𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∈ wcel 1448 ∀wral 2375 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1393 |
This theorem depends on definitions: df-bi 116 df-ral 2380 |
This theorem is referenced by: ss2rabi 3126 rabnc 3342 ssintub 3736 tron 4242 djussxp 4622 dmiin 4723 dfco2 4974 coiun 4984 tfrlem6 6143 oacl 6286 sbthlem1 6773 peano1nnnn 7539 renfdisj 7696 1nn 8589 ioomax 9572 iccmax 9573 fxnn0nninf 10052 fisumcom2 11046 bezoutlemmain 11479 dfphi2 11688 unennn 11702 znnen 11703 istopon 11962 neipsm 12105 bj-omtrans2 12740 nninfomnilem 12798 exmidsbthrlem 12801 |
Copyright terms: Public domain | W3C validator |