![]() |
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 477 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 3adantl2 1156 |
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 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: acexmid 5918 ordiso2 7096 addlocpr 7598 distrlem1prl 7644 distrlem1pru 7645 ltsopr 7658 addcanprlemu 7677 fzo1fzo0n0 10253 prodfap0 11691 prodfrecap 11692 muldvds2 11963 dvds2add 11971 dvds2sub 11972 dvdstr 11974 qusaddvallemg 12919 mulgnnsubcl 13207 mulgpropdg 13237 ringidss 13528 lmodprop2d 13847 cnpnei 14398 upxp 14451 lgsval4lem 15168 |
Copyright terms: Public domain | W3C validator |