![]() |
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 1154 |
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 980 |
This theorem is referenced by: acexmid 5873 ordiso2 7033 addlocpr 7534 distrlem1prl 7580 distrlem1pru 7581 ltsopr 7594 addcanprlemu 7613 fzo1fzo0n0 10180 prodfap0 11548 prodfrecap 11549 muldvds2 11819 dvds2add 11827 dvds2sub 11828 dvdstr 11830 qusaddvallemg 12746 mulgnnsubcl 12989 mulgpropdg 13018 ringidss 13205 cnpnei 13650 upxp 13703 lgsval4lem 14343 |
Copyright terms: Public domain | W3C validator |