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 284 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
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 is referenced by: ad2ant2l 499 ad2ant2rl 502 3ad2antr2 1132 3ad2antr3 1133 xordidc 1362 foco 5325 fvun1 5455 isocnv 5680 isores2 5682 f1oiso2 5696 offval 5957 xp2nd 6032 1stconst 6086 2ndconst 6087 tfrlem9 6184 nnmordi 6380 dom2lem 6634 fundmen 6668 mapen 6708 ssenen 6713 ltsonq 7174 ltexnqq 7184 genprndl 7297 genprndu 7298 ltpopr 7371 ltsopr 7372 ltexprlemm 7376 ltexprlemopl 7377 ltexprlemopu 7379 ltexprlemdisj 7382 ltexprlemfl 7385 ltexprlemfu 7387 mulcmpblnrlemg 7516 cnegexlem2 7906 muladd 8114 eqord1 8213 eqord2 8214 divadddivap 8455 ltmul12a 8586 lemul12b 8587 cju 8687 zextlt 9111 supinfneg 9358 infsupneg 9359 xrre 9571 ixxdisj 9654 iooshf 9703 icodisj 9743 iccshftr 9745 iccshftl 9747 iccdil 9749 icccntr 9751 iccf1o 9755 fzaddel 9807 fzsubel 9808 seq3caopr 10224 expineg2 10270 expsubap 10309 expnbnd 10383 facndiv 10453 hashfacen 10547 lcmdvds 11687 hashdvds 11824 txlm 12375 blininf 12520 xmeter 12532 xmetresbl 12536 limcimo 12730 |
Copyright terms: Public domain | W3C validator |