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 2510 | . 2 |
3 | mprgbir.1 | . 2 | |
4 | 2, 3 | mpbir 145 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wcel 2128 wral 2435 |
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 1429 |
This theorem depends on definitions: df-bi 116 df-ral 2440 |
This theorem is referenced by: ss2rabi 3210 rabnc 3426 ssintub 3825 tron 4342 djussxp 4731 dmiin 4832 dfco2 5085 coiun 5095 tfrlem6 6263 oacl 6407 sbthlem1 6901 peano1nnnn 7772 renfdisj 7937 1nn 8844 ioomax 9852 iccmax 9853 fxnn0nninf 10337 fisumcom2 11335 fprodcom2fi 11523 bezoutlemmain 11882 dfphi2 12095 unennn 12137 znnen 12138 istopon 12422 neipsm 12565 bj-omtrans2 13543 nninfomnilem 13601 exmidsbthrlem 13604 |
Copyright terms: Public domain | W3C validator |