![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > adantrl | Unicode version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
Ref | Expression |
---|---|
adant2.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
adantrl |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 109 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | adant2.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylan2 282 |
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 is referenced by: ad2ant2l 497 ad2ant2rl 500 3ad2antr2 1130 3ad2antr3 1131 xordidc 1360 foco 5313 fvun1 5441 isocnv 5666 isores2 5668 f1oiso2 5682 offval 5943 xp2nd 6018 1stconst 6072 2ndconst 6073 tfrlem9 6170 nnmordi 6366 dom2lem 6620 fundmen 6654 mapen 6693 ssenen 6698 ltsonq 7151 ltexnqq 7161 genprndl 7274 genprndu 7275 ltpopr 7348 ltsopr 7349 ltexprlemm 7353 ltexprlemopl 7354 ltexprlemopu 7356 ltexprlemdisj 7359 ltexprlemfl 7362 ltexprlemfu 7364 mulcmpblnrlemg 7480 cnegexlem2 7858 muladd 8062 eqord1 8161 eqord2 8162 divadddivap 8397 ltmul12a 8525 lemul12b 8526 cju 8626 zextlt 9044 supinfneg 9289 infsupneg 9290 xrre 9493 ixxdisj 9576 iooshf 9625 icodisj 9665 iccshftr 9667 iccshftl 9669 iccdil 9671 icccntr 9673 iccf1o 9677 fzaddel 9729 fzsubel 9730 seq3caopr 10146 expineg2 10192 expsubap 10231 expnbnd 10305 facndiv 10375 hashfacen 10469 lcmdvds 11603 hashdvds 11739 txlm 12287 blininf 12410 xmeter 12422 xmetresbl 12426 limcimo 12587 |
Copyright terms: Public domain | W3C validator |