Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3ad2antl1 | Unicode version |
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
Ref | Expression |
---|---|
3ad2antl.1 |
Ref | Expression |
---|---|
3ad2antl1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ad2antl.1 | . . 3 | |
2 | 1 | adantlr 468 | . 2 |
3 | 2 | 3adantl2 1138 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 964 |
This theorem is referenced by: acexmid 5773 ordiso2 6920 addlocpr 7344 distrlem1prl 7390 distrlem1pru 7391 ltsopr 7404 addcanprlemu 7423 fzo1fzo0n0 9960 prodfap0 11314 prodfrecap 11315 muldvds2 11519 dvds2add 11527 dvds2sub 11528 dvdstr 11530 cnpnei 12388 upxp 12441 |
Copyright terms: Public domain | W3C validator |