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 2517 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝜓 |
3 | mprgbir.1 | . 2 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) | |
4 | 2, 3 | mpbir 145 | 1 ⊢ 𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∈ wcel 2135 ∀wral 2442 |
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 1436 |
This theorem depends on definitions: df-bi 116 df-ral 2447 |
This theorem is referenced by: ss2rabi 3219 rabnc 3436 ssintub 3836 tron 4354 djussxp 4743 dmiin 4844 dfco2 5097 coiun 5107 tfrlem6 6275 oacl 6419 sbthlem1 6913 peano1nnnn 7784 renfdisj 7949 1nn 8859 ioomax 9875 iccmax 9876 fxnn0nninf 10363 fisumcom2 11365 fprodcom2fi 11553 bezoutlemmain 11916 dfphi2 12131 unennn 12273 znnen 12274 istopon 12558 neipsm 12701 bj-omtrans2 13680 nninfomnilem 13739 exmidsbthrlem 13742 |
Copyright terms: Public domain | W3C validator |