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 109 | . 2 | |
2 | adant2.1 | . 2 | |
3 | 1, 2 | sylan 281 | 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: ad2antlr 480 ad2ant2l 499 ad2ant2lr 501 3ad2antl3 1130 3adant1l 1193 reu6 2846 sbc2iegf 2951 sbcralt 2957 sbcrext 2958 indifdir 3302 pofun 4204 poinxp 4578 ssimaex 5450 fndmdif 5493 dffo4 5536 fcompt 5558 fconst2g 5603 foco2 5623 foeqcnvco 5659 f1eqcocnv 5660 fliftel1 5663 isores3 5684 acexmid 5741 tfrlemi14d 6198 tfrcl 6229 dom2lem 6634 fiintim 6785 ordiso2 6888 mkvprop 7000 lt2addnq 7180 lt2mulnq 7181 ltexnqq 7184 genpdf 7284 addnqprl 7305 addnqpru 7306 addlocpr 7312 recexprlemopl 7401 caucvgsrlemgt1 7571 add4 7891 cnegex 7908 ltleadd 8176 zextle 9110 peano5uzti 9127 fnn0ind 9135 xrlttr 9549 xaddass 9620 iccshftr 9745 iccshftl 9747 iccdil 9749 icccntr 9751 fzaddel 9807 fzrev 9832 exbtwnzlemshrink 9994 seq3val 10199 iseqf1olemab 10230 exp3vallem 10262 mulexp 10300 expadd 10303 expmul 10306 leexp1a 10316 bccl 10481 hashfacen 10547 ovshftex 10559 2shfti 10571 caucvgre 10721 cvg1nlemcau 10724 resqrexlemcvg 10759 cau3lem 10854 rexico 10961 iooinsup 11014 climmpt 11037 subcn2 11048 climrecvg1n 11085 climcvg1nlem 11086 climcaucn 11088 mertenslem2 11273 eftlcl 11321 reeftlcl 11322 dvdsext 11480 sqoddm1div8z 11510 bezoutlemaz 11618 bezoutr1 11648 dvdslcm 11677 lcmeq0 11679 lcmcl 11680 lcmneg 11682 lcmdvds 11687 coprmgcdb 11696 dvdsprime 11730 cnco 12317 cnss1 12322 tx2cn 12366 upxp 12368 metss 12590 txmetcnp 12614 cncfss 12666 cosz12 12788 bj-findis 13104 |
Copyright terms: Public domain | W3C validator |