Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > adantll | 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 |
---|---|
adantll |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 103 | . 2 | |
2 | adant2.1 | . 2 | |
3 | 1, 2 | sylan 267 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem is referenced by: ad2antlr 458 ad2ant2l 477 ad2ant2lr 479 3ad2antl3 1068 3adant1l 1127 reu6 2730 sbc2iegf 2828 sbcralt 2834 sbcrext 2835 indifdir 3193 pofun 4049 poinxp 4409 ssimaex 5234 fndmdif 5272 dffo4 5315 foco2 5318 fcompt 5333 fconst2g 5376 foeqcnvco 5430 f1eqcocnv 5431 fliftel1 5434 isores3 5455 acexmid 5511 tfrlemi14d 5947 dom2lem 6252 ordiso2 6357 lt2addnq 6502 lt2mulnq 6503 ltexnqq 6506 genpdf 6606 addnqprl 6627 addnqpru 6628 addlocpr 6634 recexprlemopl 6723 caucvgsrlemgt1 6879 add4 7172 cnegex 7189 ltleadd 7441 zextle 8331 peano5uzti 8346 fnn0ind 8354 xrlttr 8716 iccshftr 8862 iccshftl 8864 iccdil 8866 icccntr 8868 fzaddel 8922 fzrev 8946 expivallem 9256 expival 9257 mulexp 9294 expadd 9297 expmul 9300 leexp1a 9309 ovshftex 9420 2shfti 9432 caucvgre 9580 cvg1nlemcau 9583 resqrexlemcvg 9617 cau3lem 9710 climmpt 9821 subcn2 9832 climrecvg1n 9867 climcvg1nlem 9868 climcaucn 9870 bj-findis 10104 |
Copyright terms: Public domain | W3C validator |