![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpgbir | Unicode version |
Description: Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994.) (Proof shortened by Stefan Allan, 28-Oct-2008.) |
Ref | Expression |
---|---|
mpgbir.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mpgbir.2 |
![]() ![]() |
Ref | Expression |
---|---|
mpgbir |
![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpgbir.2 |
. . 3
![]() ![]() | |
2 | 1 | ax-gen 1449 |
. 2
![]() ![]() ![]() ![]() |
3 | mpgbir.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 |
This theorem is referenced by: nfi 1462 cvjust 2172 eqriv 2174 abbi2i 2292 nfci 2309 abid2f 2345 rgen 2530 ssriv 3159 ss2abi 3227 nel0 3444 ssmin 3861 intab 3871 iunab 3930 iinab 3945 sndisj 3996 disjxsn 3998 intid 4221 fr0 4348 zfregfr 4570 peano1 4590 relssi 4714 dm0 4837 dmi 4838 funopabeq 5248 isarep2 5299 fvopab3ig 5586 opabex 5736 acexmid 5868 finomni 7132 dfuzi 9352 fzodisj 10164 fzouzdisj 10166 bdelir 14255 |
Copyright terms: Public domain | W3C validator |