![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mprgbir | Unicode 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 2530 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | mprgbir.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | mpbir 146 |
1
![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
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 1449 |
This theorem depends on definitions: df-bi 117 df-ral 2460 |
This theorem is referenced by: ss2rabi 3237 rabnc 3455 ssintub 3862 tron 4382 djussxp 4772 dmiin 4873 dfco2 5128 coiun 5138 tfrlem6 6316 oacl 6460 sbthlem1 6955 peano1nnnn 7850 renfdisj 8015 1nn 8928 ioomax 9946 iccmax 9947 fxnn0nninf 10435 fisumcom2 11441 fprodcom2fi 11629 bezoutlemmain 11993 dfphi2 12214 unennn 12392 znnen 12393 istopon 13444 neipsm 13585 bj-omtrans2 14629 nninfomnilem 14687 exmidsbthrlem 14690 |
Copyright terms: Public domain | W3C validator |