![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3adant3r | Unicode version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) |
Ref | Expression |
---|---|
3adant1l.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3adant3r |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3adant1l.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3com13 1154 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 3adant1r 1177 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | 3com13 1154 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 932 |
This theorem is referenced by: addassnqg 7091 mulassnqg 7093 prarloc 7212 ltpopr 7304 ltexprlemfl 7318 ltexprlemfu 7320 addasssrg 7452 axaddass 7557 apmul1 8409 ltmul2 8472 lemul2 8473 dvdscmulr 11317 dvdsmulcr 11318 modremain 11421 ndvdsadd 11423 rpexp12i 11626 xblcntrps 12341 xblcntr 12342 |
Copyright terms: Public domain | W3C validator |