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 500 ad2ant2rl 503 3ad2antr2 1152 3ad2antr3 1153 xordidc 1388 foco 5414 fvun1 5546 isocnv 5773 isores2 5775 f1oiso2 5789 offval 6051 xp2nd 6126 1stconst 6180 2ndconst 6181 tfrlem9 6278 nnmordi 6475 dom2lem 6729 fundmen 6763 mapen 6803 ssenen 6808 ltsonq 7330 ltexnqq 7340 genprndl 7453 genprndu 7454 ltpopr 7527 ltsopr 7528 ltexprlemm 7532 ltexprlemopl 7533 ltexprlemopu 7535 ltexprlemdisj 7538 ltexprlemfl 7541 ltexprlemfu 7543 mulcmpblnrlemg 7672 cnegexlem2 8065 muladd 8273 eqord1 8372 eqord2 8373 divadddivap 8614 ltmul12a 8746 lemul12b 8747 cju 8847 zextlt 9274 supinfneg 9524 infsupneg 9525 xrre 9747 ixxdisj 9830 iooshf 9879 icodisj 9919 iccshftr 9921 iccshftl 9923 iccdil 9925 icccntr 9927 iccf1o 9931 fzaddel 9984 fzsubel 9985 seq3caopr 10408 expineg2 10454 expsubap 10493 expnbnd 10567 facndiv 10641 hashfacen 10735 fprodeq0 11544 lcmdvds 11990 hashdvds 12132 eulerthlemh 12142 pceu 12206 pcqcl 12217 txlm 12826 blininf 12971 xmeter 12983 xmetresbl 12987 limcimo 13181 |
Copyright terms: Public domain | W3C validator |