Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > adantllr | Unicode version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.) |
Ref | Expression |
---|---|
adantl2.1 |
Ref | Expression |
---|---|
adantllr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 108 | . 2 | |
2 | adantl2.1 | . 2 | |
3 | 1, 2 | sylanl1 400 | 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: ad4ant13 510 ad4ant134 1212 r19.29an 2612 diffifi 6869 fimax2gtrilemstep 6875 cnegexlem3 8085 cnegex 8086 lemul12b 8766 climshftlemg 11254 prodeq2 11509 fprodmodd 11593 lcmdvds 12022 pw2dvdslemn 12108 tgcl 12819 metss 13249 ivthinclemlr 13370 ivthinclemur 13372 |
Copyright terms: Public domain | W3C validator |