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 2523 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝜓 |
3 | mprgbir.1 | . 2 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) | |
4 | 2, 3 | mpbir 145 | 1 ⊢ 𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∈ wcel 2141 ∀wral 2448 |
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 1442 |
This theorem depends on definitions: df-bi 116 df-ral 2453 |
This theorem is referenced by: ss2rabi 3229 rabnc 3446 ssintub 3847 tron 4365 djussxp 4754 dmiin 4855 dfco2 5108 coiun 5118 tfrlem6 6293 oacl 6437 sbthlem1 6932 peano1nnnn 7807 renfdisj 7972 1nn 8882 ioomax 9898 iccmax 9899 fxnn0nninf 10387 fisumcom2 11394 fprodcom2fi 11582 bezoutlemmain 11946 dfphi2 12167 unennn 12345 znnen 12346 istopon 12770 neipsm 12913 bj-omtrans2 13957 nninfomnilem 14016 exmidsbthrlem 14019 |
Copyright terms: Public domain | W3C validator |