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 1429 | . 2 |
3 | mpgbir.1 | . 2 | |
4 | 2, 3 | mpbir 145 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wal 1333 |
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 |
This theorem is referenced by: nfi 1442 cvjust 2152 eqriv 2154 abbi2i 2272 nfci 2289 abid2f 2325 rgen 2510 ssriv 3132 ss2abi 3200 nel0 3415 ssmin 3826 intab 3836 iunab 3895 iinab 3910 sndisj 3961 disjxsn 3963 intid 4184 fr0 4311 zfregfr 4533 peano1 4553 relssi 4677 dm0 4800 dmi 4801 funopabeq 5206 isarep2 5257 fvopab3ig 5542 opabex 5691 acexmid 5823 finomni 7083 dfuzi 9274 fzodisj 10077 fzouzdisj 10079 bdelir 13422 |
Copyright terms: Public domain | W3C validator |